(set-info :smt-lib-version 2.6)
(set-logic QF_UF)
(set-info :source |
http://www.cs.bham.ac.uk/~vxs/quasigroups/benchmark/

|)
(set-info :category "crafted")
(set-info :status unsat)
(declare-sort U 0)
(declare-sort I 0)
(declare-fun unit () I)
(declare-fun op (I I) I)
(declare-fun e5 () I)
(declare-fun e4 () I)
(declare-fun e3 () I)
(declare-fun e2 () I)
(declare-fun e1 () I)
(declare-fun e0 () I)
(assert (let ((?v_0 (op e0 e0)) (?v_1 (op e0 e1)) (?v_2 (op e0 e2)) (?v_3 (op e0 e3)) (?v_4 (op e0 e4)) (?v_5 (op e0 e5)) (?v_6 (op e1 e0)) (?v_7 (op e1 e1)) (?v_8 (op e1 e2)) (?v_9 (op e1 e3)) (?v_10 (op e1 e4)) (?v_11 (op e1 e5)) (?v_12 (op e2 e0)) (?v_13 (op e2 e1)) (?v_14 (op e2 e2)) (?v_15 (op e2 e3)) (?v_16 (op e2 e4)) (?v_17 (op e2 e5)) (?v_18 (op e3 e0)) (?v_19 (op e3 e1)) (?v_20 (op e3 e2)) (?v_21 (op e3 e3)) (?v_22 (op e3 e4)) (?v_23 (op e3 e5)) (?v_24 (op e4 e0)) (?v_25 (op e4 e1)) (?v_26 (op e4 e2)) (?v_27 (op e4 e3)) (?v_28 (op e4 e4)) (?v_29 (op e4 e5)) (?v_30 (op e5 e0)) (?v_31 (op e5 e1)) (?v_32 (op e5 e2)) (?v_33 (op e5 e3)) (?v_34 (op e5 e4)) (?v_35 (op e5 e5))) (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or (= ?v_0 e0) (= ?v_0 e1)) (= ?v_0 e2)) (= ?v_0 e3)) (= ?v_0 e4)) (= ?v_0 e5)) (or (or (or (or (or (= ?v_1 e0) (= ?v_1 e1)) (= ?v_1 e2)) (= ?v_1 e3)) (= ?v_1 e4)) (= ?v_1 e5))) (or (or (or (or (or (= ?v_2 e0) (= ?v_2 e1)) (= ?v_2 e2)) (= ?v_2 e3)) (= ?v_2 e4)) (= ?v_2 e5))) (or (or (or (or (or (= ?v_3 e0) (= ?v_3 e1)) (= ?v_3 e2)) (= ?v_3 e3)) (= ?v_3 e4)) (= ?v_3 e5))) (or (or (or (or (or (= ?v_4 e0) (= ?v_4 e1)) (= ?v_4 e2)) (= ?v_4 e3)) (= ?v_4 e4)) (= ?v_4 e5))) (or (or (or (or (or (= ?v_5 e0) (= ?v_5 e1)) (= ?v_5 e2)) (= ?v_5 e3)) (= ?v_5 e4)) (= ?v_5 e5))) (and (and (and (and (and (or (or (or (or (or (= ?v_6 e0) (= ?v_6 e1)) (= ?v_6 e2)) (= ?v_6 e3)) (= ?v_6 e4)) (= ?v_6 e5)) (or (or (or (or (or (= ?v_7 e0) (= ?v_7 e1)) (= ?v_7 e2)) (= ?v_7 e3)) (= ?v_7 e4)) (= ?v_7 e5))) (or (or (or (or (or (= ?v_8 e0) (= ?v_8 e1)) (= ?v_8 e2)) (= ?v_8 e3)) (= ?v_8 e4)) (= ?v_8 e5))) (or (or (or (or (or (= ?v_9 e0) (= ?v_9 e1)) (= ?v_9 e2)) (= ?v_9 e3)) (= ?v_9 e4)) (= ?v_9 e5))) (or (or (or (or (or (= ?v_10 e0) (= ?v_10 e1)) (= ?v_10 e2)) (= ?v_10 e3)) (= ?v_10 e4)) (= ?v_10 e5))) (or (or (or (or (or (= ?v_11 e0) (= ?v_11 e1)) (= ?v_11 e2)) (= ?v_11 e3)) (= ?v_11 e4)) (= ?v_11 e5)))) (and (and (and (and (and (or (or (or (or (or (= ?v_12 e0) (= ?v_12 e1)) (= ?v_12 e2)) (= ?v_12 e3)) (= ?v_12 e4)) (= ?v_12 e5)) (or (or (or (or (or (= ?v_13 e0) (= ?v_13 e1)) (= ?v_13 e2)) (= ?v_13 e3)) (= ?v_13 e4)) (= ?v_13 e5))) (or (or (or (or (or (= ?v_14 e0) (= ?v_14 e1)) (= ?v_14 e2)) (= ?v_14 e3)) (= ?v_14 e4)) (= ?v_14 e5))) (or (or (or (or (or (= ?v_15 e0) (= ?v_15 e1)) (= ?v_15 e2)) (= ?v_15 e3)) (= ?v_15 e4)) (= ?v_15 e5))) (or (or (or (or (or (= ?v_16 e0) (= ?v_16 e1)) (= ?v_16 e2)) (= ?v_16 e3)) (= ?v_16 e4)) (= ?v_16 e5))) (or (or (or (or (or (= ?v_17 e0) (= ?v_17 e1)) (= ?v_17 e2)) (= ?v_17 e3)) (= ?v_17 e4)) (= ?v_17 e5)))) (and (and (and (and (and (or (or (or (or (or (= ?v_18 e0) (= ?v_18 e1)) (= ?v_18 e2)) (= ?v_18 e3)) (= ?v_18 e4)) (= ?v_18 e5)) (or (or (or (or (or (= ?v_19 e0) (= ?v_19 e1)) (= ?v_19 e2)) (= ?v_19 e3)) (= ?v_19 e4)) (= ?v_19 e5))) (or (or (or (or (or (= ?v_20 e0) (= ?v_20 e1)) (= ?v_20 e2)) (= ?v_20 e3)) (= ?v_20 e4)) (= ?v_20 e5))) (or (or (or (or (or (= ?v_21 e0) (= ?v_21 e1)) (= ?v_21 e2)) (= ?v_21 e3)) (= ?v_21 e4)) (= ?v_21 e5))) (or (or (or (or (or (= ?v_22 e0) (= ?v_22 e1)) (= ?v_22 e2)) (= ?v_22 e3)) (= ?v_22 e4)) (= ?v_22 e5))) (or (or (or (or (or (= ?v_23 e0) (= ?v_23 e1)) (= ?v_23 e2)) (= ?v_23 e3)) (= ?v_23 e4)) (= ?v_23 e5)))) (and (and (and (and (and (or (or (or (or (or (= ?v_24 e0) (= ?v_24 e1)) (= ?v_24 e2)) (= ?v_24 e3)) (= ?v_24 e4)) (= ?v_24 e5)) (or (or (or (or (or (= ?v_25 e0) (= ?v_25 e1)) (= ?v_25 e2)) (= ?v_25 e3)) (= ?v_25 e4)) (= ?v_25 e5))) (or (or (or (or (or (= ?v_26 e0) (= ?v_26 e1)) (= ?v_26 e2)) (= ?v_26 e3)) (= ?v_26 e4)) (= ?v_26 e5))) (or (or (or (or (or (= ?v_27 e0) (= ?v_27 e1)) (= ?v_27 e2)) (= ?v_27 e3)) (= ?v_27 e4)) (= ?v_27 e5))) (or (or (or (or (or (= ?v_28 e0) (= ?v_28 e1)) (= ?v_28 e2)) (= ?v_28 e3)) (= ?v_28 e4)) (= ?v_28 e5))) (or (or (or (or (or (= ?v_29 e0) (= ?v_29 e1)) (= ?v_29 e2)) (= ?v_29 e3)) (= ?v_29 e4)) (= ?v_29 e5)))) (and (and (and (and (and (or (or (or (or (or (= ?v_30 e0) (= ?v_30 e1)) (= ?v_30 e2)) (= ?v_30 e3)) (= ?v_30 e4)) (= ?v_30 e5)) (or (or (or (or (or (= ?v_31 e0) (= ?v_31 e1)) (= ?v_31 e2)) (= ?v_31 e3)) (= ?v_31 e4)) (= ?v_31 e5))) (or (or (or (or (or (= ?v_32 e0) (= ?v_32 e1)) (= ?v_32 e2)) (= ?v_32 e3)) (= ?v_32 e4)) (= ?v_32 e5))) (or (or (or (or (or (= ?v_33 e0) (= ?v_33 e1)) (= ?v_33 e2)) (= ?v_33 e3)) (= ?v_33 e4)) (= ?v_33 e5))) (or (or (or (or (or (= ?v_34 e0) (= ?v_34 e1)) (= ?v_34 e2)) (= ?v_34 e3)) (= ?v_34 e4)) (= ?v_34 e5))) (or (or (or (or (or (= ?v_35 e0) (= ?v_35 e1)) (= ?v_35 e2)) (= ?v_35 e3)) (= ?v_35 e4)) (= ?v_35 e5))))))
(assert (let ((?v_1 (op e0 e0)) (?v_2 (op e0 e1)) (?v_3 (op e0 e2)) (?v_4 (op e0 e3)) (?v_5 (op e0 e4)) (?v_6 (op e0 e5)) (?v_8 (op e1 e0)) (?v_21 (op e1 e1)) (?v_22 (op e1 e2)) (?v_23 (op e1 e3)) (?v_24 (op e1 e4)) (?v_25 (op e1 e5)) (?v_9 (op e2 e0)) (?v_28 (op e2 e1)) (?v_51 (op e2 e2)) (?v_52 (op e2 e3)) (?v_53 (op e2 e4)) (?v_54 (op e2 e5)) (?v_10 (op e3 e0)) (?v_29 (op e3 e1)) (?v_58 (op e3 e2)) (?v_91 (op e3 e3)) (?v_92 (op e3 e4)) (?v_93 (op e3 e5)) (?v_11 (op e4 e0)) (?v_30 (op e4 e1)) (?v_59 (op e4 e2)) (?v_98 (op e4 e3)) (?v_141 (op e4 e4)) (?v_142 (op e4 e5)) (?v_12 (op e5 e0)) (?v_31 (op e5 e1)) (?v_60 (op e5 e2)) (?v_99 (op e5 e3)) (?v_148 (op e5 e4)) (?v_201 (op e5 e5))) (let ((?v_0 (= ?v_1 e0)) (?v_7 (= ?v_1 e1)) (?v_13 (= ?v_1 e2)) (?v_14 (= ?v_1 e3)) (?v_15 (= ?v_1 e4)) (?v_16 (= ?v_1 e5)) (?v_18 (= ?v_2 e0)) (?v_26 (= ?v_2 e1)) (?v_33 (= ?v_2 e2)) (?v_36 (= ?v_2 e3)) (?v_39 (= ?v_2 e4)) (?v_42 (= ?v_2 e5)) (?v_46 (= ?v_3 e0)) (?v_55 (= ?v_3 e1)) (?v_63 (= ?v_3 e2)) (?v_68 (= ?v_3 e3)) (?v_73 (= ?v_3 e4)) (?v_78 (= ?v_3 e5)) (?v_84 (= ?v_4 e0)) (?v_94 (= ?v_4 e1)) (?v_103 (= ?v_4 e2)) (?v_110 (= ?v_4 e3)) (?v_117 (= ?v_4 e4)) (?v_124 (= ?v_4 e5)) (?v_132 (= ?v_5 e0)) (?v_143 (= ?v_5 e1)) (?v_153 (= ?v_5 e2)) (?v_162 (= ?v_5 e3)) (?v_171 (= ?v_5 e4)) (?v_180 (= ?v_5 e5)) (?v_190 (= ?v_6 e0)) (?v_202 (= ?v_6 e1)) (?v_213 (= ?v_6 e2)) (?v_224 (= ?v_6 e3)) (?v_235 (= ?v_6 e4)) (?v_246 (= ?v_6 e5)) (?v_17 (= ?v_8 e0)) (?v_20 (= ?v_8 e1)) (?v_32 (= ?v_8 e2)) (?v_35 (= ?v_8 e3)) (?v_38 (= ?v_8 e4)) (?v_41 (= ?v_8 e5)) (?v_19 (= ?v_21 e0)) (?v_27 (= ?v_21 e1)) (?v_34 (= ?v_21 e2)) (?v_37 (= ?v_21 e3)) (?v_40 (= ?v_21 e4)) (?v_43 (= ?v_21 e5)) (?v_47 (= ?v_22 e0)) (?v_56 (= ?v_22 e1)) (?v_64 (= ?v_22 e2)) (?v_69 (= ?v_22 e3)) (?v_74 (= ?v_22 e4)) (?v_79 (= ?v_22 e5)) (?v_85 (= ?v_23 e0)) (?v_95 (= ?v_23 e1)) (?v_104 (= ?v_23 e2)) (?v_111 (= ?v_23 e3)) (?v_118 (= ?v_23 e4)) (?v_125 (= ?v_23 e5)) (?v_133 (= ?v_24 e0)) (?v_144 (= ?v_24 e1)) (?v_154 (= ?v_24 e2)) (?v_163 (= ?v_24 e3)) (?v_172 (= ?v_24 e4)) (?v_181 (= ?v_24 e5)) (?v_191 (= ?v_25 e0)) (?v_203 (= ?v_25 e1)) (?v_214 (= ?v_25 e2)) (?v_225 (= ?v_25 e3)) (?v_236 (= ?v_25 e4)) (?v_247 (= ?v_25 e5)) (?v_44 (= ?v_9 e0)) (?v_49 (= ?v_9 e1)) (?v_61 (= ?v_9 e2)) (?v_66 (= ?v_9 e3)) (?v_71 (= ?v_9 e4)) (?v_76 (= ?v_9 e5)) (?v_45 (= ?v_28 e0)) (?v_50 (= ?v_28 e1)) (?v_62 (= ?v_28 e2)) (?v_67 (= ?v_28 e3)) (?v_72 (= ?v_28 e4)) (?v_77 (= ?v_28 e5)) (?v_48 (= ?v_51 e0)) (?v_57 (= ?v_51 e1)) (?v_65 (= ?v_51 e2)) (?v_70 (= ?v_51 e3)) (?v_75 (= ?v_51 e4)) (?v_80 (= ?v_51 e5)) (?v_86 (= ?v_52 e0)) (?v_96 (= ?v_52 e1)) (?v_105 (= ?v_52 e2)) (?v_112 (= ?v_52 e3)) (?v_119 (= ?v_52 e4)) (?v_126 (= ?v_52 e5)) (?v_134 (= ?v_53 e0)) (?v_145 (= ?v_53 e1)) (?v_155 (= ?v_53 e2)) (?v_164 (= ?v_53 e3)) (?v_173 (= ?v_53 e4)) (?v_182 (= ?v_53 e5)) (?v_192 (= ?v_54 e0)) (?v_204 (= ?v_54 e1)) (?v_215 (= ?v_54 e2)) (?v_226 (= ?v_54 e3)) (?v_237 (= ?v_54 e4)) (?v_248 (= ?v_54 e5)) (?v_81 (= ?v_10 e0)) (?v_88 (= ?v_10 e1)) (?v_100 (= ?v_10 e2)) (?v_107 (= ?v_10 e3)) (?v_114 (= ?v_10 e4)) (?v_121 (= ?v_10 e5)) (?v_82 (= ?v_29 e0)) (?v_89 (= ?v_29 e1)) (?v_101 (= ?v_29 e2)) (?v_108 (= ?v_29 e3)) (?v_115 (= ?v_29 e4)) (?v_122 (= ?v_29 e5)) (?v_83 (= ?v_58 e0)) (?v_90 (= ?v_58 e1)) (?v_102 (= ?v_58 e2)) (?v_109 (= ?v_58 e3)) (?v_116 (= ?v_58 e4)) (?v_123 (= ?v_58 e5)) (?v_87 (= ?v_91 e0)) (?v_97 (= ?v_91 e1)) (?v_106 (= ?v_91 e2)) (?v_113 (= ?v_91 e3)) (?v_120 (= ?v_91 e4)) (?v_127 (= ?v_91 e5)) (?v_135 (= ?v_92 e0)) (?v_146 (= ?v_92 e1)) (?v_156 (= ?v_92 e2)) (?v_165 (= ?v_92 e3)) (?v_174 (= ?v_92 e4)) (?v_183 (= ?v_92 e5)) (?v_193 (= ?v_93 e0)) (?v_205 (= ?v_93 e1)) (?v_216 (= ?v_93 e2)) (?v_227 (= ?v_93 e3)) (?v_238 (= ?v_93 e4)) (?v_249 (= ?v_93 e5)) (?v_128 (= ?v_11 e0)) (?v_137 (= ?v_11 e1)) (?v_149 (= ?v_11 e2)) (?v_158 (= ?v_11 e3)) (?v_167 (= ?v_11 e4)) (?v_176 (= ?v_11 e5)) (?v_129 (= ?v_30 e0)) (?v_138 (= ?v_30 e1)) (?v_150 (= ?v_30 e2)) (?v_159 (= ?v_30 e3)) (?v_168 (= ?v_30 e4)) (?v_177 (= ?v_30 e5)) (?v_130 (= ?v_59 e0)) (?v_139 (= ?v_59 e1)) (?v_151 (= ?v_59 e2)) (?v_160 (= ?v_59 e3)) (?v_169 (= ?v_59 e4)) (?v_178 (= ?v_59 e5)) (?v_131 (= ?v_98 e0)) (?v_140 (= ?v_98 e1)) (?v_152 (= ?v_98 e2)) (?v_161 (= ?v_98 e3)) (?v_170 (= ?v_98 e4)) (?v_179 (= ?v_98 e5)) (?v_136 (= ?v_141 e0)) (?v_147 (= ?v_141 e1)) (?v_157 (= ?v_141 e2)) (?v_166 (= ?v_141 e3)) (?v_175 (= ?v_141 e4)) (?v_184 (= ?v_141 e5)) (?v_194 (= ?v_142 e0)) (?v_206 (= ?v_142 e1)) (?v_217 (= ?v_142 e2)) (?v_228 (= ?v_142 e3)) (?v_239 (= ?v_142 e4)) (?v_250 (= ?v_142 e5)) (?v_185 (= ?v_12 e0)) (?v_196 (= ?v_12 e1)) (?v_208 (= ?v_12 e2)) (?v_219 (= ?v_12 e3)) (?v_230 (= ?v_12 e4)) (?v_241 (= ?v_12 e5)) (?v_186 (= ?v_31 e0)) (?v_197 (= ?v_31 e1)) (?v_209 (= ?v_31 e2)) (?v_220 (= ?v_31 e3)) (?v_231 (= ?v_31 e4)) (?v_242 (= ?v_31 e5)) (?v_187 (= ?v_60 e0)) (?v_198 (= ?v_60 e1)) (?v_210 (= ?v_60 e2)) (?v_221 (= ?v_60 e3)) (?v_232 (= ?v_60 e4)) (?v_243 (= ?v_60 e5)) (?v_188 (= ?v_99 e0)) (?v_199 (= ?v_99 e1)) (?v_211 (= ?v_99 e2)) (?v_222 (= ?v_99 e3)) (?v_233 (= ?v_99 e4)) (?v_244 (= ?v_99 e5)) (?v_189 (= ?v_148 e0)) (?v_200 (= ?v_148 e1)) (?v_212 (= ?v_148 e2)) (?v_223 (= ?v_148 e3)) (?v_234 (= ?v_148 e4)) (?v_245 (= ?v_148 e5)) (?v_195 (= ?v_201 e0)) (?v_207 (= ?v_201 e1)) (?v_218 (= ?v_201 e2)) (?v_229 (= ?v_201 e3)) (?v_240 (= ?v_201 e4)) (?v_251 (= ?v_201 e5))) (and (and (and (and (and (and (and (and (and (and (and (or (or (or (or (or ?v_0 ?v_18) ?v_46) ?v_84) ?v_132) ?v_190) (or (or (or (or (or ?v_0 ?v_17) ?v_44) ?v_81) ?v_128) ?v_185)) (and (or (or (or (or (or ?v_7 ?v_26) ?v_55) ?v_94) ?v_143) ?v_202) (or (or (or (or (or ?v_7 ?v_20) ?v_49) ?v_88) ?v_137) ?v_196))) (and (or (or (or (or (or ?v_13 ?v_33) ?v_63) ?v_103) ?v_153) ?v_213) (or (or (or (or (or ?v_13 ?v_32) ?v_61) ?v_100) ?v_149) ?v_208))) (and (or (or (or (or (or ?v_14 ?v_36) ?v_68) ?v_110) ?v_162) ?v_224) (or (or (or (or (or ?v_14 ?v_35) ?v_66) ?v_107) ?v_158) ?v_219))) (and (or (or (or (or (or ?v_15 ?v_39) ?v_73) ?v_117) ?v_171) ?v_235) (or (or (or (or (or ?v_15 ?v_38) ?v_71) ?v_114) ?v_167) ?v_230))) (and (or (or (or (or (or ?v_16 ?v_42) ?v_78) ?v_124) ?v_180) ?v_246) (or (or (or (or (or ?v_16 ?v_41) ?v_76) ?v_121) ?v_176) ?v_241))) (and (and (and (and (and (and (or (or (or (or (or ?v_17 ?v_19) ?v_47) ?v_85) ?v_133) ?v_191) (or (or (or (or (or ?v_18 ?v_19) ?v_45) ?v_82) ?v_129) ?v_186)) (and (or (or (or (or (or ?v_20 ?v_27) ?v_56) ?v_95) ?v_144) ?v_203) (or (or (or (or (or ?v_26 ?v_27) ?v_50) ?v_89) ?v_138) ?v_197))) (and (or (or (or (or (or ?v_32 ?v_34) ?v_64) ?v_104) ?v_154) ?v_214) (or (or (or (or (or ?v_33 ?v_34) ?v_62) ?v_101) ?v_150) ?v_209))) (and (or (or (or (or (or ?v_35 ?v_37) ?v_69) ?v_111) ?v_163) ?v_225) (or (or (or (or (or ?v_36 ?v_37) ?v_67) ?v_108) ?v_159) ?v_220))) (and (or (or (or (or (or ?v_38 ?v_40) ?v_74) ?v_118) ?v_172) ?v_236) (or (or (or (or (or ?v_39 ?v_40) ?v_72) ?v_115) ?v_168) ?v_231))) (and (or (or (or (or (or ?v_41 ?v_43) ?v_79) ?v_125) ?v_181) ?v_247) (or (or (or (or (or ?v_42 ?v_43) ?v_77) ?v_122) ?v_177) ?v_242)))) (and (and (and (and (and (and (or (or (or (or (or ?v_44 ?v_45) ?v_48) ?v_86) ?v_134) ?v_192) (or (or (or (or (or ?v_46 ?v_47) ?v_48) ?v_83) ?v_130) ?v_187)) (and (or (or (or (or (or ?v_49 ?v_50) ?v_57) ?v_96) ?v_145) ?v_204) (or (or (or (or (or ?v_55 ?v_56) ?v_57) ?v_90) ?v_139) ?v_198))) (and (or (or (or (or (or ?v_61 ?v_62) ?v_65) ?v_105) ?v_155) ?v_215) (or (or (or (or (or ?v_63 ?v_64) ?v_65) ?v_102) ?v_151) ?v_210))) (and (or (or (or (or (or ?v_66 ?v_67) ?v_70) ?v_112) ?v_164) ?v_226) (or (or (or (or (or ?v_68 ?v_69) ?v_70) ?v_109) ?v_160) ?v_221))) (and (or (or (or (or (or ?v_71 ?v_72) ?v_75) ?v_119) ?v_173) ?v_237) (or (or (or (or (or ?v_73 ?v_74) ?v_75) ?v_116) ?v_169) ?v_232))) (and (or (or (or (or (or ?v_76 ?v_77) ?v_80) ?v_126) ?v_182) ?v_248) (or (or (or (or (or ?v_78 ?v_79) ?v_80) ?v_123) ?v_178) ?v_243)))) (and (and (and (and (and (and (or (or (or (or (or ?v_81 ?v_82) ?v_83) ?v_87) ?v_135) ?v_193) (or (or (or (or (or ?v_84 ?v_85) ?v_86) ?v_87) ?v_131) ?v_188)) (and (or (or (or (or (or ?v_88 ?v_89) ?v_90) ?v_97) ?v_146) ?v_205) (or (or (or (or (or ?v_94 ?v_95) ?v_96) ?v_97) ?v_140) ?v_199))) (and (or (or (or (or (or ?v_100 ?v_101) ?v_102) ?v_106) ?v_156) ?v_216) (or (or (or (or (or ?v_103 ?v_104) ?v_105) ?v_106) ?v_152) ?v_211))) (and (or (or (or (or (or ?v_107 ?v_108) ?v_109) ?v_113) ?v_165) ?v_227) (or (or (or (or (or ?v_110 ?v_111) ?v_112) ?v_113) ?v_161) ?v_222))) (and (or (or (or (or (or ?v_114 ?v_115) ?v_116) ?v_120) ?v_174) ?v_238) (or (or (or (or (or ?v_117 ?v_118) ?v_119) ?v_120) ?v_170) ?v_233))) (and (or (or (or (or (or ?v_121 ?v_122) ?v_123) ?v_127) ?v_183) ?v_249) (or (or (or (or (or ?v_124 ?v_125) ?v_126) ?v_127) ?v_179) ?v_244)))) (and (and (and (and (and (and (or (or (or (or (or ?v_128 ?v_129) ?v_130) ?v_131) ?v_136) ?v_194) (or (or (or (or (or ?v_132 ?v_133) ?v_134) ?v_135) ?v_136) ?v_189)) (and (or (or (or (or (or ?v_137 ?v_138) ?v_139) ?v_140) ?v_147) ?v_206) (or (or (or (or (or ?v_143 ?v_144) ?v_145) ?v_146) ?v_147) ?v_200))) (and (or (or (or (or (or ?v_149 ?v_150) ?v_151) ?v_152) ?v_157) ?v_217) (or (or (or (or (or ?v_153 ?v_154) ?v_155) ?v_156) ?v_157) ?v_212))) (and (or (or (or (or (or ?v_158 ?v_159) ?v_160) ?v_161) ?v_166) ?v_228) (or (or (or (or (or ?v_162 ?v_163) ?v_164) ?v_165) ?v_166) ?v_223))) (and (or (or (or (or (or ?v_167 ?v_168) ?v_169) ?v_170) ?v_175) ?v_239) (or (or (or (or (or ?v_171 ?v_172) ?v_173) ?v_174) ?v_175) ?v_234))) (and (or (or (or (or (or ?v_176 ?v_177) ?v_178) ?v_179) ?v_184) ?v_250) (or (or (or (or (or ?v_180 ?v_181) ?v_182) ?v_183) ?v_184) ?v_245)))) (and (and (and (and (and (and (or (or (or (or (or ?v_185 ?v_186) ?v_187) ?v_188) ?v_189) ?v_195) (or (or (or (or (or ?v_190 ?v_191) ?v_192) ?v_193) ?v_194) ?v_195)) (and (or (or (or (or (or ?v_196 ?v_197) ?v_198) ?v_199) ?v_200) ?v_207) (or (or (or (or (or ?v_202 ?v_203) ?v_204) ?v_205) ?v_206) ?v_207))) (and (or (or (or (or (or ?v_208 ?v_209) ?v_210) ?v_211) ?v_212) ?v_218) (or (or (or (or (or ?v_213 ?v_214) ?v_215) ?v_216) ?v_217) ?v_218))) (and (or (or (or (or (or ?v_219 ?v_220) ?v_221) ?v_222) ?v_223) ?v_229) (or (or (or (or (or ?v_224 ?v_225) ?v_226) ?v_227) ?v_228) ?v_229))) (and (or (or (or (or (or ?v_230 ?v_231) ?v_232) ?v_233) ?v_234) ?v_240) (or (or (or (or (or ?v_235 ?v_236) ?v_237) ?v_238) ?v_239) ?v_240))) (and (or (or (or (or (or ?v_241 ?v_242) ?v_243) ?v_244) ?v_245) ?v_251) (or (or (or (or (or ?v_246 ?v_247) ?v_248) ?v_249) ?v_250) ?v_251)))))))
(assert (and (and (and (and (and (and (and (= (op unit e0) e0) (= (op e0 unit) e0)) (and (= (op unit e1) e1) (= (op e1 unit) e1))) (and (= (op unit e2) e2) (= (op e2 unit) e2))) (and (= (op unit e3) e3) (= (op e3 unit) e3))) (and (= (op unit e4) e4) (= (op e4 unit) e4))) (and (= (op unit e5) e5) (= (op e5 unit) e5))) (or (or (or (or (or (= unit e0) (= unit e1)) (= unit e2)) (= unit e3)) (= unit e4)) (= unit e5))))
(assert (let ((?v_0 (op e0 e0)) (?v_1 (op e0 e1)) (?v_4 (op e0 e2)) (?v_9 (op e0 e3)) (?v_16 (op e0 e4)) (?v_25 (op e0 e5)) (?v_2 (op e1 e0)) (?v_3 (op e1 e1)) (?v_6 (op e1 e2)) (?v_11 (op e1 e3)) (?v_18 (op e1 e4)) (?v_27 (op e1 e5)) (?v_5 (op e2 e0)) (?v_7 (op e2 e1)) (?v_8 (op e2 e2)) (?v_13 (op e2 e3)) (?v_20 (op e2 e4)) (?v_29 (op e2 e5)) (?v_10 (op e3 e0)) (?v_12 (op e3 e1)) (?v_14 (op e3 e2)) (?v_15 (op e3 e3)) (?v_22 (op e3 e4)) (?v_31 (op e3 e5)) (?v_17 (op e4 e0)) (?v_19 (op e4 e1)) (?v_21 (op e4 e2)) (?v_23 (op e4 e3)) (?v_24 (op e4 e4)) (?v_33 (op e4 e5)) (?v_26 (op e5 e0)) (?v_28 (op e5 e1)) (?v_30 (op e5 e2)) (?v_32 (op e5 e3)) (?v_34 (op e5 e4)) (?v_35 (op e5 e5))) (or (or (or (or (or (or (or (or (or (or (not (= ?v_0 ?v_0)) (not (= ?v_2 ?v_1))) (not (= ?v_5 ?v_4))) (not (= ?v_10 ?v_9))) (not (= ?v_17 ?v_16))) (not (= ?v_26 ?v_25))) (or (or (or (or (or (not (= ?v_1 ?v_2)) (not (= ?v_3 ?v_3))) (not (= ?v_7 ?v_6))) (not (= ?v_12 ?v_11))) (not (= ?v_19 ?v_18))) (not (= ?v_28 ?v_27)))) (or (or (or (or (or (not (= ?v_4 ?v_5)) (not (= ?v_6 ?v_7))) (not (= ?v_8 ?v_8))) (not (= ?v_14 ?v_13))) (not (= ?v_21 ?v_20))) (not (= ?v_30 ?v_29)))) (or (or (or (or (or (not (= ?v_9 ?v_10)) (not (= ?v_11 ?v_12))) (not (= ?v_13 ?v_14))) (not (= ?v_15 ?v_15))) (not (= ?v_23 ?v_22))) (not (= ?v_32 ?v_31)))) (or (or (or (or (or (not (= ?v_16 ?v_17)) (not (= ?v_18 ?v_19))) (not (= ?v_20 ?v_21))) (not (= ?v_22 ?v_23))) (not (= ?v_24 ?v_24))) (not (= ?v_34 ?v_33)))) (or (or (or (or (or (not (= ?v_25 ?v_26)) (not (= ?v_27 ?v_28))) (not (= ?v_29 ?v_30))) (not (= ?v_31 ?v_32))) (not (= ?v_33 ?v_34))) (not (= ?v_35 ?v_35))))))
(assert (and (and (and (and (and (or (or (or (or (or (= (op (op e0 e0) e0) e0) (= (op (op e0 e1) e0) e1)) (= (op (op e0 e2) e0) e2)) (= (op (op e0 e3) e0) e3)) (= (op (op e0 e4) e0) e4)) (= (op (op e0 e5) e0) e5)) (or (or (or (or (or (= (op (op e1 e0) e1) e0) (= (op (op e1 e1) e1) e1)) (= (op (op e1 e2) e1) e2)) (= (op (op e1 e3) e1) e3)) (= (op (op e1 e4) e1) e4)) (= (op (op e1 e5) e1) e5))) (or (or (or (or (or (= (op (op e2 e0) e2) e0) (= (op (op e2 e1) e2) e1)) (= (op (op e2 e2) e2) e2)) (= (op (op e2 e3) e2) e3)) (= (op (op e2 e4) e2) e4)) (= (op (op e2 e5) e2) e5))) (or (or (or (or (or (= (op (op e3 e0) e3) e0) (= (op (op e3 e1) e3) e1)) (= (op (op e3 e2) e3) e2)) (= (op (op e3 e3) e3) e3)) (= (op (op e3 e4) e3) e4)) (= (op (op e3 e5) e3) e5))) (or (or (or (or (or (= (op (op e4 e0) e4) e0) (= (op (op e4 e1) e4) e1)) (= (op (op e4 e2) e4) e2)) (= (op (op e4 e3) e4) e3)) (= (op (op e4 e4) e4) e4)) (= (op (op e4 e5) e4) e5))) (or (or (or (or (or (= (op (op e5 e0) e5) e0) (= (op (op e5 e1) e5) e1)) (= (op (op e5 e2) e5) e2)) (= (op (op e5 e3) e5) e3)) (= (op (op e5 e4) e5) e4)) (= (op (op e5 e5) e5) e5))))
(assert (and (and (and (and (and (or (or (or (or (or (not (= (op (op e0 e0) e0) e0)) (not (= (op (op e1 e0) e1) e0))) (not (= (op (op e2 e0) e2) e0))) (not (= (op (op e3 e0) e3) e0))) (not (= (op (op e4 e0) e4) e0))) (not (= (op (op e5 e0) e5) e0))) (or (or (or (or (or (not (= (op (op e0 e1) e0) e1)) (not (= (op (op e1 e1) e1) e1))) (not (= (op (op e2 e1) e2) e1))) (not (= (op (op e3 e1) e3) e1))) (not (= (op (op e4 e1) e4) e1))) (not (= (op (op e5 e1) e5) e1)))) (or (or (or (or (or (not (= (op (op e0 e2) e0) e2)) (not (= (op (op e1 e2) e1) e2))) (not (= (op (op e2 e2) e2) e2))) (not (= (op (op e3 e2) e3) e2))) (not (= (op (op e4 e2) e4) e2))) (not (= (op (op e5 e2) e5) e2)))) (or (or (or (or (or (not (= (op (op e0 e3) e0) e3)) (not (= (op (op e1 e3) e1) e3))) (not (= (op (op e2 e3) e2) e3))) (not (= (op (op e3 e3) e3) e3))) (not (= (op (op e4 e3) e4) e3))) (not (= (op (op e5 e3) e5) e3)))) (or (or (or (or (or (not (= (op (op e0 e4) e0) e4)) (not (= (op (op e1 e4) e1) e4))) (not (= (op (op e2 e4) e2) e4))) (not (= (op (op e3 e4) e3) e4))) (not (= (op (op e4 e4) e4) e4))) (not (= (op (op e5 e4) e5) e4)))) (or (or (or (or (or (not (= (op (op e0 e5) e0) e5)) (not (= (op (op e1 e5) e1) e5))) (not (= (op (op e2 e5) e2) e5))) (not (= (op (op e3 e5) e3) e5))) (not (= (op (op e4 e5) e4) e5))) (not (= (op (op e5 e5) e5) e5)))))
(assert (let ((?v_1 (op e0 e0)) (?v_3 (op e0 e1)) (?v_5 (op e0 e2)) (?v_7 (op e0 e3)) (?v_9 (op e0 e4)) (?v_11 (op e0 e5)) (?v_15 (op e1 e0)) (?v_22 (op e1 e1)) (?v_24 (op e1 e2)) (?v_25 (op e1 e3)) (?v_26 (op e1 e4)) (?v_27 (op e1 e5)) (?v_28 (op e2 e0)) (?v_30 (op e2 e1)) (?v_32 (op e2 e2)) (?v_33 (op e2 e3)) (?v_34 (op e2 e4)) (?v_35 (op e2 e5)) (?v_36 (op e3 e0)) (?v_38 (op e3 e1)) (?v_40 (op e3 e2)) (?v_41 (op e3 e3)) (?v_42 (op e3 e4)) (?v_43 (op e3 e5)) (?v_44 (op e4 e0)) (?v_46 (op e4 e1)) (?v_48 (op e4 e2)) (?v_49 (op e4 e3)) (?v_50 (op e4 e4)) (?v_51 (op e4 e5)) (?v_52 (op e5 e0)) (?v_54 (op e5 e1)) (?v_56 (op e5 e2)) (?v_57 (op e5 e3)) (?v_58 (op e5 e4)) (?v_59 (op e5 e5))) (let ((?v_0 (= ?v_1 e0)) (?v_12 (= ?v_1 e1)) (?v_60 (= ?v_1 e2)) (?v_90 (= ?v_1 e3)) (?v_132 (= ?v_1 e4)) (?v_186 (= ?v_1 e5)) (?v_2 (= ?v_3 e0)) (?v_14 (= ?v_3 e1)) (?v_62 (= ?v_3 e2)) (?v_92 (= ?v_3 e3)) (?v_134 (= ?v_3 e4)) (?v_188 (= ?v_3 e5)) (?v_4 (= ?v_5 e0)) (?v_16 (= ?v_5 e1)) (?v_64 (= ?v_5 e2)) (?v_94 (= ?v_5 e3)) (?v_136 (= ?v_5 e4)) (?v_190 (= ?v_5 e5)) (?v_6 (= ?v_7 e0)) (?v_17 (= ?v_7 e1)) (?v_65 (= ?v_7 e2)) (?v_96 (= ?v_7 e3)) (?v_138 (= ?v_7 e4)) (?v_192 (= ?v_7 e5)) (?v_8 (= ?v_9 e0)) (?v_18 (= ?v_9 e1)) (?v_66 (= ?v_9 e2)) (?v_97 (= ?v_9 e3)) (?v_140 (= ?v_9 e4)) (?v_194 (= ?v_9 e5)) (?v_10 (= ?v_11 e0)) (?v_19 (= ?v_11 e1)) (?v_67 (= ?v_11 e2)) (?v_98 (= ?v_11 e3)) (?v_141 (= ?v_11 e4)) (?v_196 (= ?v_11 e5)) (?v_13 (= ?v_15 e0)) (?v_20 (= ?v_15 e1)) (?v_68 (= ?v_15 e2)) (?v_99 (= ?v_15 e3)) (?v_142 (= ?v_15 e4)) (?v_197 (= ?v_15 e5)) (?v_21 (= ?v_22 e0)) (?v_23 (= ?v_22 e1)) (?v_70 (= ?v_22 e2)) (?v_101 (= ?v_22 e3)) (?v_144 (= ?v_22 e4)) (?v_199 (= ?v_22 e5)) (?v_29 (= ?v_24 e0)) (?v_31 (= ?v_24 e1)) (?v_72 (= ?v_24 e2)) (?v_103 (= ?v_24 e3)) (?v_146 (= ?v_24 e4)) (?v_201 (= ?v_24 e5)) (?v_37 (= ?v_25 e0)) (?v_39 (= ?v_25 e1)) (?v_73 (= ?v_25 e2)) (?v_105 (= ?v_25 e3)) (?v_148 (= ?v_25 e4)) (?v_203 (= ?v_25 e5)) (?v_45 (= ?v_26 e0)) (?v_47 (= ?v_26 e1)) (?v_74 (= ?v_26 e2)) (?v_106 (= ?v_26 e3)) (?v_150 (= ?v_26 e4)) (?v_205 (= ?v_26 e5)) (?v_53 (= ?v_27 e0)) (?v_55 (= ?v_27 e1)) (?v_75 (= ?v_27 e2)) (?v_107 (= ?v_27 e3)) (?v_151 (= ?v_27 e4)) (?v_207 (= ?v_27 e5)) (?v_61 (= ?v_28 e0)) (?v_63 (= ?v_28 e1)) (?v_76 (= ?v_28 e2)) (?v_108 (= ?v_28 e3)) (?v_152 (= ?v_28 e4)) (?v_208 (= ?v_28 e5)) (?v_69 (= ?v_30 e0)) (?v_71 (= ?v_30 e1)) (?v_78 (= ?v_30 e2)) (?v_110 (= ?v_30 e3)) (?v_154 (= ?v_30 e4)) (?v_210 (= ?v_30 e5)) (?v_77 (= ?v_32 e0)) (?v_79 (= ?v_32 e1)) (?v_80 (= ?v_32 e2)) (?v_112 (= ?v_32 e3)) (?v_156 (= ?v_32 e4)) (?v_212 (= ?v_32 e5)) (?v_81 (= ?v_33 e0)) (?v_82 (= ?v_33 e1)) (?v_83 (= ?v_33 e2)) (?v_114 (= ?v_33 e3)) (?v_158 (= ?v_33 e4)) (?v_214 (= ?v_33 e5)) (?v_84 (= ?v_34 e0)) (?v_85 (= ?v_34 e1)) (?v_86 (= ?v_34 e2)) (?v_115 (= ?v_34 e3)) (?v_160 (= ?v_34 e4)) (?v_216 (= ?v_34 e5)) (?v_87 (= ?v_35 e0)) (?v_88 (= ?v_35 e1)) (?v_89 (= ?v_35 e2)) (?v_116 (= ?v_35 e3)) (?v_161 (= ?v_35 e4)) (?v_218 (= ?v_35 e5)) (?v_91 (= ?v_36 e0)) (?v_93 (= ?v_36 e1)) (?v_95 (= ?v_36 e2)) (?v_117 (= ?v_36 e3)) (?v_162 (= ?v_36 e4)) (?v_219 (= ?v_36 e5)) (?v_100 (= ?v_38 e0)) (?v_102 (= ?v_38 e1)) (?v_104 (= ?v_38 e2)) (?v_119 (= ?v_38 e3)) (?v_164 (= ?v_38 e4)) (?v_221 (= ?v_38 e5)) (?v_109 (= ?v_40 e0)) (?v_111 (= ?v_40 e1)) (?v_113 (= ?v_40 e2)) (?v_121 (= ?v_40 e3)) (?v_166 (= ?v_40 e4)) (?v_223 (= ?v_40 e5)) (?v_118 (= ?v_41 e0)) (?v_120 (= ?v_41 e1)) (?v_122 (= ?v_41 e2)) (?v_123 (= ?v_41 e3)) (?v_168 (= ?v_41 e4)) (?v_225 (= ?v_41 e5)) (?v_124 (= ?v_42 e0)) (?v_125 (= ?v_42 e1)) (?v_126 (= ?v_42 e2)) (?v_127 (= ?v_42 e3)) (?v_170 (= ?v_42 e4)) (?v_227 (= ?v_42 e5)) (?v_128 (= ?v_43 e0)) (?v_129 (= ?v_43 e1)) (?v_130 (= ?v_43 e2)) (?v_131 (= ?v_43 e3)) (?v_171 (= ?v_43 e4)) (?v_229 (= ?v_43 e5)) (?v_133 (= ?v_44 e0)) (?v_135 (= ?v_44 e1)) (?v_137 (= ?v_44 e2)) (?v_139 (= ?v_44 e3)) (?v_172 (= ?v_44 e4)) (?v_230 (= ?v_44 e5)) (?v_143 (= ?v_46 e0)) (?v_145 (= ?v_46 e1)) (?v_147 (= ?v_46 e2)) (?v_149 (= ?v_46 e3)) (?v_174 (= ?v_46 e4)) (?v_232 (= ?v_46 e5)) (?v_153 (= ?v_48 e0)) (?v_155 (= ?v_48 e1)) (?v_157 (= ?v_48 e2)) (?v_159 (= ?v_48 e3)) (?v_176 (= ?v_48 e4)) (?v_234 (= ?v_48 e5)) (?v_163 (= ?v_49 e0)) (?v_165 (= ?v_49 e1)) (?v_167 (= ?v_49 e2)) (?v_169 (= ?v_49 e3)) (?v_178 (= ?v_49 e4)) (?v_236 (= ?v_49 e5)) (?v_173 (= ?v_50 e0)) (?v_175 (= ?v_50 e1)) (?v_177 (= ?v_50 e2)) (?v_179 (= ?v_50 e3)) (?v_180 (= ?v_50 e4)) (?v_238 (= ?v_50 e5)) (?v_181 (= ?v_51 e0)) (?v_182 (= ?v_51 e1)) (?v_183 (= ?v_51 e2)) (?v_184 (= ?v_51 e3)) (?v_185 (= ?v_51 e4)) (?v_240 (= ?v_51 e5)) (?v_187 (= ?v_52 e0)) (?v_189 (= ?v_52 e1)) (?v_191 (= ?v_52 e2)) (?v_193 (= ?v_52 e3)) (?v_195 (= ?v_52 e4)) (?v_241 (= ?v_52 e5)) (?v_198 (= ?v_54 e0)) (?v_200 (= ?v_54 e1)) (?v_202 (= ?v_54 e2)) (?v_204 (= ?v_54 e3)) (?v_206 (= ?v_54 e4)) (?v_243 (= ?v_54 e5)) (?v_209 (= ?v_56 e0)) (?v_211 (= ?v_56 e1)) (?v_213 (= ?v_56 e2)) (?v_215 (= ?v_56 e3)) (?v_217 (= ?v_56 e4)) (?v_245 (= ?v_56 e5)) (?v_220 (= ?v_57 e0)) (?v_222 (= ?v_57 e1)) (?v_224 (= ?v_57 e2)) (?v_226 (= ?v_57 e3)) (?v_228 (= ?v_57 e4)) (?v_247 (= ?v_57 e5)) (?v_231 (= ?v_58 e0)) (?v_233 (= ?v_58 e1)) (?v_235 (= ?v_58 e2)) (?v_237 (= ?v_58 e3)) (?v_239 (= ?v_58 e4)) (?v_249 (= ?v_58 e5)) (?v_242 (= ?v_59 e0)) (?v_244 (= ?v_59 e1)) (?v_246 (= ?v_59 e2)) (?v_248 (= ?v_59 e3)) (?v_250 (= ?v_59 e4)) (?v_251 (= ?v_59 e5))) (and (and (and (and (and (or (or (or (or (or (or (or (or (or (or (and ?v_0 (not ?v_0)) (and ?v_2 (not ?v_12))) (and ?v_4 (not ?v_60))) (and ?v_6 (not ?v_90))) (and ?v_8 (not ?v_132))) (and ?v_10 (not ?v_186))) (or (or (or (or (or (and ?v_13 (not ?v_2)) (and ?v_21 (not ?v_14))) (and ?v_29 (not ?v_62))) (and ?v_37 (not ?v_92))) (and ?v_45 (not ?v_134))) (and ?v_53 (not ?v_188)))) (or (or (or (or (or (and ?v_61 (not ?v_4)) (and ?v_69 (not ?v_16))) (and ?v_77 (not ?v_64))) (and ?v_81 (not ?v_94))) (and ?v_84 (not ?v_136))) (and ?v_87 (not ?v_190)))) (or (or (or (or (or (and ?v_91 (not ?v_6)) (and ?v_100 (not ?v_17))) (and ?v_109 (not ?v_65))) (and ?v_118 (not ?v_96))) (and ?v_124 (not ?v_138))) (and ?v_128 (not ?v_192)))) (or (or (or (or (or (and ?v_133 (not ?v_8)) (and ?v_143 (not ?v_18))) (and ?v_153 (not ?v_66))) (and ?v_163 (not ?v_97))) (and ?v_173 (not ?v_140))) (and ?v_181 (not ?v_194)))) (or (or (or (or (or (and ?v_187 (not ?v_10)) (and ?v_198 (not ?v_19))) (and ?v_209 (not ?v_67))) (and ?v_220 (not ?v_98))) (and ?v_231 (not ?v_141))) (and ?v_242 (not ?v_196)))) (or (or (or (or (or (or (or (or (or (or (and ?v_12 (not ?v_13)) (and ?v_14 (not ?v_20))) (and ?v_16 (not ?v_68))) (and ?v_17 (not ?v_99))) (and ?v_18 (not ?v_142))) (and ?v_19 (not ?v_197))) (or (or (or (or (or (and ?v_20 (not ?v_21)) (and ?v_23 (not ?v_23))) (and ?v_31 (not ?v_70))) (and ?v_39 (not ?v_101))) (and ?v_47 (not ?v_144))) (and ?v_55 (not ?v_199)))) (or (or (or (or (or (and ?v_63 (not ?v_29)) (and ?v_71 (not ?v_31))) (and ?v_79 (not ?v_72))) (and ?v_82 (not ?v_103))) (and ?v_85 (not ?v_146))) (and ?v_88 (not ?v_201)))) (or (or (or (or (or (and ?v_93 (not ?v_37)) (and ?v_102 (not ?v_39))) (and ?v_111 (not ?v_73))) (and ?v_120 (not ?v_105))) (and ?v_125 (not ?v_148))) (and ?v_129 (not ?v_203)))) (or (or (or (or (or (and ?v_135 (not ?v_45)) (and ?v_145 (not ?v_47))) (and ?v_155 (not ?v_74))) (and ?v_165 (not ?v_106))) (and ?v_175 (not ?v_150))) (and ?v_182 (not ?v_205)))) (or (or (or (or (or (and ?v_189 (not ?v_53)) (and ?v_200 (not ?v_55))) (and ?v_211 (not ?v_75))) (and ?v_222 (not ?v_107))) (and ?v_233 (not ?v_151))) (and ?v_244 (not ?v_207))))) (or (or (or (or (or (or (or (or (or (or (and ?v_60 (not ?v_61)) (and ?v_62 (not ?v_63))) (and ?v_64 (not ?v_76))) (and ?v_65 (not ?v_108))) (and ?v_66 (not ?v_152))) (and ?v_67 (not ?v_208))) (or (or (or (or (or (and ?v_68 (not ?v_69)) (and ?v_70 (not ?v_71))) (and ?v_72 (not ?v_78))) (and ?v_73 (not ?v_110))) (and ?v_74 (not ?v_154))) (and ?v_75 (not ?v_210)))) (or (or (or (or (or (and ?v_76 (not ?v_77)) (and ?v_78 (not ?v_79))) (and ?v_80 (not ?v_80))) (and ?v_83 (not ?v_112))) (and ?v_86 (not ?v_156))) (and ?v_89 (not ?v_212)))) (or (or (or (or (or (and ?v_95 (not ?v_81)) (and ?v_104 (not ?v_82))) (and ?v_113 (not ?v_83))) (and ?v_122 (not ?v_114))) (and ?v_126 (not ?v_158))) (and ?v_130 (not ?v_214)))) (or (or (or (or (or (and ?v_137 (not ?v_84)) (and ?v_147 (not ?v_85))) (and ?v_157 (not ?v_86))) (and ?v_167 (not ?v_115))) (and ?v_177 (not ?v_160))) (and ?v_183 (not ?v_216)))) (or (or (or (or (or (and ?v_191 (not ?v_87)) (and ?v_202 (not ?v_88))) (and ?v_213 (not ?v_89))) (and ?v_224 (not ?v_116))) (and ?v_235 (not ?v_161))) (and ?v_246 (not ?v_218))))) (or (or (or (or (or (or (or (or (or (or (and ?v_90 (not ?v_91)) (and ?v_92 (not ?v_93))) (and ?v_94 (not ?v_95))) (and ?v_96 (not ?v_117))) (and ?v_97 (not ?v_162))) (and ?v_98 (not ?v_219))) (or (or (or (or (or (and ?v_99 (not ?v_100)) (and ?v_101 (not ?v_102))) (and ?v_103 (not ?v_104))) (and ?v_105 (not ?v_119))) (and ?v_106 (not ?v_164))) (and ?v_107 (not ?v_221)))) (or (or (or (or (or (and ?v_108 (not ?v_109)) (and ?v_110 (not ?v_111))) (and ?v_112 (not ?v_113))) (and ?v_114 (not ?v_121))) (and ?v_115 (not ?v_166))) (and ?v_116 (not ?v_223)))) (or (or (or (or (or (and ?v_117 (not ?v_118)) (and ?v_119 (not ?v_120))) (and ?v_121 (not ?v_122))) (and ?v_123 (not ?v_123))) (and ?v_127 (not ?v_168))) (and ?v_131 (not ?v_225)))) (or (or (or (or (or (and ?v_139 (not ?v_124)) (and ?v_149 (not ?v_125))) (and ?v_159 (not ?v_126))) (and ?v_169 (not ?v_127))) (and ?v_179 (not ?v_170))) (and ?v_184 (not ?v_227)))) (or (or (or (or (or (and ?v_193 (not ?v_128)) (and ?v_204 (not ?v_129))) (and ?v_215 (not ?v_130))) (and ?v_226 (not ?v_131))) (and ?v_237 (not ?v_171))) (and ?v_248 (not ?v_229))))) (or (or (or (or (or (or (or (or (or (or (and ?v_132 (not ?v_133)) (and ?v_134 (not ?v_135))) (and ?v_136 (not ?v_137))) (and ?v_138 (not ?v_139))) (and ?v_140 (not ?v_172))) (and ?v_141 (not ?v_230))) (or (or (or (or (or (and ?v_142 (not ?v_143)) (and ?v_144 (not ?v_145))) (and ?v_146 (not ?v_147))) (and ?v_148 (not ?v_149))) (and ?v_150 (not ?v_174))) (and ?v_151 (not ?v_232)))) (or (or (or (or (or (and ?v_152 (not ?v_153)) (and ?v_154 (not ?v_155))) (and ?v_156 (not ?v_157))) (and ?v_158 (not ?v_159))) (and ?v_160 (not ?v_176))) (and ?v_161 (not ?v_234)))) (or (or (or (or (or (and ?v_162 (not ?v_163)) (and ?v_164 (not ?v_165))) (and ?v_166 (not ?v_167))) (and ?v_168 (not ?v_169))) (and ?v_170 (not ?v_178))) (and ?v_171 (not ?v_236)))) (or (or (or (or (or (and ?v_172 (not ?v_173)) (and ?v_174 (not ?v_175))) (and ?v_176 (not ?v_177))) (and ?v_178 (not ?v_179))) (and ?v_180 (not ?v_180))) (and ?v_185 (not ?v_238)))) (or (or (or (or (or (and ?v_195 (not ?v_181)) (and ?v_206 (not ?v_182))) (and ?v_217 (not ?v_183))) (and ?v_228 (not ?v_184))) (and ?v_239 (not ?v_185))) (and ?v_250 (not ?v_240))))) (or (or (or (or (or (or (or (or (or (or (and ?v_186 (not ?v_187)) (and ?v_188 (not ?v_189))) (and ?v_190 (not ?v_191))) (and ?v_192 (not ?v_193))) (and ?v_194 (not ?v_195))) (and ?v_196 (not ?v_241))) (or (or (or (or (or (and ?v_197 (not ?v_198)) (and ?v_199 (not ?v_200))) (and ?v_201 (not ?v_202))) (and ?v_203 (not ?v_204))) (and ?v_205 (not ?v_206))) (and ?v_207 (not ?v_243)))) (or (or (or (or (or (and ?v_208 (not ?v_209)) (and ?v_210 (not ?v_211))) (and ?v_212 (not ?v_213))) (and ?v_214 (not ?v_215))) (and ?v_216 (not ?v_217))) (and ?v_218 (not ?v_245)))) (or (or (or (or (or (and ?v_219 (not ?v_220)) (and ?v_221 (not ?v_222))) (and ?v_223 (not ?v_224))) (and ?v_225 (not ?v_226))) (and ?v_227 (not ?v_228))) (and ?v_229 (not ?v_247)))) (or (or (or (or (or (and ?v_230 (not ?v_231)) (and ?v_232 (not ?v_233))) (and ?v_234 (not ?v_235))) (and ?v_236 (not ?v_237))) (and ?v_238 (not ?v_239))) (and ?v_240 (not ?v_249)))) (or (or (or (or (or (and ?v_241 (not ?v_242)) (and ?v_243 (not ?v_244))) (and ?v_245 (not ?v_246))) (and ?v_247 (not ?v_248))) (and ?v_249 (not ?v_250))) (and ?v_251 (not ?v_251))))))))
(assert (let ((?v_0 (op e0 e0)) (?v_1 (op e0 e1)) (?v_2 (op e0 e2)) (?v_3 (op e0 e3)) (?v_4 (op e0 e4)) (?v_5 (op e0 e5)) (?v_6 (op e1 e0)) (?v_7 (op e1 e1)) (?v_8 (op e1 e2)) (?v_9 (op e1 e3)) (?v_10 (op e1 e4)) (?v_11 (op e1 e5)) (?v_12 (op e2 e0)) (?v_13 (op e2 e1)) (?v_14 (op e2 e2)) (?v_15 (op e2 e3)) (?v_16 (op e2 e4)) (?v_17 (op e2 e5)) (?v_18 (op e3 e0)) (?v_19 (op e3 e1)) (?v_20 (op e3 e2)) (?v_21 (op e3 e3)) (?v_22 (op e3 e4)) (?v_23 (op e3 e5)) (?v_24 (op e4 e0)) (?v_25 (op e4 e1)) (?v_26 (op e4 e2)) (?v_27 (op e4 e3)) (?v_28 (op e4 e4)) (?v_29 (op e4 e5)) (?v_30 (op e5 e0)) (?v_31 (op e5 e1)) (?v_32 (op e5 e2)) (?v_33 (op e5 e3)) (?v_34 (op e5 e4)) (?v_35 (op e5 e5))) (or (or (or (or (or (and (and (and (and (and (not (= (op ?v_0 ?v_0) e0)) (not (= (op ?v_1 ?v_1) e1))) (not (= (op ?v_2 ?v_2) e2))) (not (= (op ?v_3 ?v_3) e3))) (not (= (op ?v_4 ?v_4) e4))) (not (= (op ?v_5 ?v_5) e5))) (and (and (and (and (and (not (= (op ?v_6 ?v_6) e0)) (not (= (op ?v_7 ?v_7) e1))) (not (= (op ?v_8 ?v_8) e2))) (not (= (op ?v_9 ?v_9) e3))) (not (= (op ?v_10 ?v_10) e4))) (not (= (op ?v_11 ?v_11) e5)))) (and (and (and (and (and (not (= (op ?v_12 ?v_12) e0)) (not (= (op ?v_13 ?v_13) e1))) (not (= (op ?v_14 ?v_14) e2))) (not (= (op ?v_15 ?v_15) e3))) (not (= (op ?v_16 ?v_16) e4))) (not (= (op ?v_17 ?v_17) e5)))) (and (and (and (and (and (not (= (op ?v_18 ?v_18) e0)) (not (= (op ?v_19 ?v_19) e1))) (not (= (op ?v_20 ?v_20) e2))) (not (= (op ?v_21 ?v_21) e3))) (not (= (op ?v_22 ?v_22) e4))) (not (= (op ?v_23 ?v_23) e5)))) (and (and (and (and (and (not (= (op ?v_24 ?v_24) e0)) (not (= (op ?v_25 ?v_25) e1))) (not (= (op ?v_26 ?v_26) e2))) (not (= (op ?v_27 ?v_27) e3))) (not (= (op ?v_28 ?v_28) e4))) (not (= (op ?v_29 ?v_29) e5)))) (and (and (and (and (and (not (= (op ?v_30 ?v_30) e0)) (not (= (op ?v_31 ?v_31) e1))) (not (= (op ?v_32 ?v_32) e2))) (not (= (op ?v_33 ?v_33) e3))) (not (= (op ?v_34 ?v_34) e4))) (not (= (op ?v_35 ?v_35) e5))))))
(assert (or (or (or (or (or (and (and (and (and (and (not (= (op e0 (op e0 e0)) e0)) (not (= (op e0 (op e0 e1)) e1))) (not (= (op e0 (op e0 e2)) e2))) (not (= (op e0 (op e0 e3)) e3))) (not (= (op e0 (op e0 e4)) e4))) (not (= (op e0 (op e0 e5)) e5))) (and (and (and (and (and (not (= (op e1 (op e1 e0)) e0)) (not (= (op e1 (op e1 e1)) e1))) (not (= (op e1 (op e1 e2)) e2))) (not (= (op e1 (op e1 e3)) e3))) (not (= (op e1 (op e1 e4)) e4))) (not (= (op e1 (op e1 e5)) e5)))) (and (and (and (and (and (not (= (op e2 (op e2 e0)) e0)) (not (= (op e2 (op e2 e1)) e1))) (not (= (op e2 (op e2 e2)) e2))) (not (= (op e2 (op e2 e3)) e3))) (not (= (op e2 (op e2 e4)) e4))) (not (= (op e2 (op e2 e5)) e5)))) (and (and (and (and (and (not (= (op e3 (op e3 e0)) e0)) (not (= (op e3 (op e3 e1)) e1))) (not (= (op e3 (op e3 e2)) e2))) (not (= (op e3 (op e3 e3)) e3))) (not (= (op e3 (op e3 e4)) e4))) (not (= (op e3 (op e3 e5)) e5)))) (and (and (and (and (and (not (= (op e4 (op e4 e0)) e0)) (not (= (op e4 (op e4 e1)) e1))) (not (= (op e4 (op e4 e2)) e2))) (not (= (op e4 (op e4 e3)) e3))) (not (= (op e4 (op e4 e4)) e4))) (not (= (op e4 (op e4 e5)) e5)))) (and (and (and (and (and (not (= (op e5 (op e5 e0)) e0)) (not (= (op e5 (op e5 e1)) e1))) (not (= (op e5 (op e5 e2)) e2))) (not (= (op e5 (op e5 e3)) e3))) (not (= (op e5 (op e5 e4)) e4))) (not (= (op e5 (op e5 e5)) e5)))))
(assert (let ((?v_0 (op e0 e0)) (?v_6 (op e0 e1)) (?v_12 (op e0 e2)) (?v_18 (op e0 e3)) (?v_24 (op e0 e4)) (?v_30 (op e0 e5)) (?v_1 (op e1 e0)) (?v_7 (op e1 e1)) (?v_13 (op e1 e2)) (?v_19 (op e1 e3)) (?v_25 (op e1 e4)) (?v_31 (op e1 e5)) (?v_2 (op e2 e0)) (?v_8 (op e2 e1)) (?v_14 (op e2 e2)) (?v_20 (op e2 e3)) (?v_26 (op e2 e4)) (?v_32 (op e2 e5)) (?v_3 (op e3 e0)) (?v_9 (op e3 e1)) (?v_15 (op e3 e2)) (?v_21 (op e3 e3)) (?v_27 (op e3 e4)) (?v_33 (op e3 e5)) (?v_4 (op e4 e0)) (?v_10 (op e4 e1)) (?v_16 (op e4 e2)) (?v_22 (op e4 e3)) (?v_28 (op e4 e4)) (?v_34 (op e4 e5)) (?v_5 (op e5 e0)) (?v_11 (op e5 e1)) (?v_17 (op e5 e2)) (?v_23 (op e5 e3)) (?v_29 (op e5 e4)) (?v_35 (op e5 e5))) (or (or (or (or (or (and (and (and (and (and (not (= (op ?v_0 ?v_0) e0)) (not (= (op ?v_1 ?v_1) e1))) (not (= (op ?v_2 ?v_2) e2))) (not (= (op ?v_3 ?v_3) e3))) (not (= (op ?v_4 ?v_4) e4))) (not (= (op ?v_5 ?v_5) e5))) (and (and (and (and (and (not (= (op ?v_6 ?v_6) e0)) (not (= (op ?v_7 ?v_7) e1))) (not (= (op ?v_8 ?v_8) e2))) (not (= (op ?v_9 ?v_9) e3))) (not (= (op ?v_10 ?v_10) e4))) (not (= (op ?v_11 ?v_11) e5)))) (and (and (and (and (and (not (= (op ?v_12 ?v_12) e0)) (not (= (op ?v_13 ?v_13) e1))) (not (= (op ?v_14 ?v_14) e2))) (not (= (op ?v_15 ?v_15) e3))) (not (= (op ?v_16 ?v_16) e4))) (not (= (op ?v_17 ?v_17) e5)))) (and (and (and (and (and (not (= (op ?v_18 ?v_18) e0)) (not (= (op ?v_19 ?v_19) e1))) (not (= (op ?v_20 ?v_20) e2))) (not (= (op ?v_21 ?v_21) e3))) (not (= (op ?v_22 ?v_22) e4))) (not (= (op ?v_23 ?v_23) e5)))) (and (and (and (and (and (not (= (op ?v_24 ?v_24) e0)) (not (= (op ?v_25 ?v_25) e1))) (not (= (op ?v_26 ?v_26) e2))) (not (= (op ?v_27 ?v_27) e3))) (not (= (op ?v_28 ?v_28) e4))) (not (= (op ?v_29 ?v_29) e5)))) (and (and (and (and (and (not (= (op ?v_30 ?v_30) e0)) (not (= (op ?v_31 ?v_31) e1))) (not (= (op ?v_32 ?v_32) e2))) (not (= (op ?v_33 ?v_33) e3))) (not (= (op ?v_34 ?v_34) e4))) (not (= (op ?v_35 ?v_35) e5))))))
(assert (let ((?v_2 (op e0 e0)) (?v_51 (op e0 e1)) (?v_54 (op e0 e2)) (?v_56 (op e0 e3)) (?v_58 (op e0 e4)) (?v_60 (op e0 e5)) (?v_6 (op e1 e0)) (?v_65 (op e1 e1)) (?v_68 (op e1 e2)) (?v_70 (op e1 e3)) (?v_72 (op e1 e4)) (?v_74 (op e1 e5)) (?v_12 (op e2 e0)) (?v_69 (op e2 e1)) (?v_82 (op e2 e2)) (?v_84 (op e2 e3)) (?v_86 (op e2 e4)) (?v_88 (op e2 e5)) (?v_19 (op e3 e0)) (?v_71 (op e3 e1)) (?v_85 (op e3 e2)) (?v_98 (op e3 e3)) (?v_100 (op e3 e4)) (?v_102 (op e3 e5)) (?v_28 (op e4 e0)) (?v_73 (op e4 e1)) (?v_87 (op e4 e2)) (?v_101 (op e4 e3)) (?v_114 (op e4 e4)) (?v_116 (op e4 e5)) (?v_39 (op e5 e0)) (?v_75 (op e5 e1)) (?v_89 (op e5 e2)) (?v_103 (op e5 e3)) (?v_117 (op e5 e4)) (?v_130 (op e5 e5))) (let ((?v_0 (= ?v_2 e0)) (?v_48 (= ?v_2 e1)) (?v_132 (= ?v_2 e2)) (?v_198 (= ?v_2 e3)) (?v_276 (= ?v_2 e4)) (?v_366 (= ?v_2 e5)) (?v_49 (= ?v_51 e0)) (?v_52 (= ?v_51 e1)) (?v_135 (= ?v_51 e2)) (?v_201 (= ?v_51 e3)) (?v_279 (= ?v_51 e4)) (?v_369 (= ?v_51 e5)) (?v_133 (= ?v_54 e0)) (?v_136 (= ?v_54 e1)) (?v_138 (= ?v_54 e2)) (?v_204 (= ?v_54 e3)) (?v_282 (= ?v_54 e4)) (?v_372 (= ?v_54 e5)) (?v_199 (= ?v_56 e0)) (?v_202 (= ?v_56 e1)) (?v_205 (= ?v_56 e2)) (?v_207 (= ?v_56 e3)) (?v_285 (= ?v_56 e4)) (?v_375 (= ?v_56 e5)) (?v_277 (= ?v_58 e0)) (?v_280 (= ?v_58 e1)) (?v_283 (= ?v_58 e2)) (?v_286 (= ?v_58 e3)) (?v_288 (= ?v_58 e4)) (?v_378 (= ?v_58 e5)) (?v_367 (= ?v_60 e0)) (?v_370 (= ?v_60 e1)) (?v_373 (= ?v_60 e2)) (?v_376 (= ?v_60 e3)) (?v_379 (= ?v_60 e4)) (?v_381 (= ?v_60 e5)) (?v_4 (= ?v_6 e0)) (?v_53 (= ?v_6 e1)) (?v_137 (= ?v_6 e2)) (?v_203 (= ?v_6 e3)) (?v_281 (= ?v_6 e4)) (?v_371 (= ?v_6 e5)) (?v_63 (= ?v_65 e0)) (?v_66 (= ?v_65 e1)) (?v_146 (= ?v_65 e2)) (?v_214 (= ?v_65 e3)) (?v_294 (= ?v_65 e4)) (?v_386 (= ?v_65 e5)) (?v_144 (= ?v_68 e0)) (?v_147 (= ?v_68 e1)) (?v_149 (= ?v_68 e2)) (?v_217 (= ?v_68 e3)) (?v_297 (= ?v_68 e4)) (?v_389 (= ?v_68 e5)) (?v_212 (= ?v_70 e0)) (?v_215 (= ?v_70 e1)) (?v_218 (= ?v_70 e2)) (?v_220 (= ?v_70 e3)) (?v_300 (= ?v_70 e4)) (?v_392 (= ?v_70 e5)) (?v_292 (= ?v_72 e0)) (?v_295 (= ?v_72 e1)) (?v_298 (= ?v_72 e2)) (?v_301 (= ?v_72 e3)) (?v_303 (= ?v_72 e4)) (?v_395 (= ?v_72 e5)) (?v_384 (= ?v_74 e0)) (?v_387 (= ?v_74 e1)) (?v_390 (= ?v_74 e2)) (?v_393 (= ?v_74 e3)) (?v_396 (= ?v_74 e4)) (?v_398 (= ?v_74 e5)) (?v_9 (= ?v_12 e0)) (?v_55 (= ?v_12 e1)) (?v_139 (= ?v_12 e2)) (?v_206 (= ?v_12 e3)) (?v_284 (= ?v_12 e4)) (?v_374 (= ?v_12 e5)) (?v_77 (= ?v_69 e0)) (?v_80 (= ?v_69 e1)) (?v_150 (= ?v_69 e2)) (?v_219 (= ?v_69 e3)) (?v_299 (= ?v_69 e4)) (?v_391 (= ?v_69 e5)) (?v_155 (= ?v_82 e0)) (?v_158 (= ?v_82 e1)) (?v_160 (= ?v_82 e2)) (?v_230 (= ?v_82 e3)) (?v_312 (= ?v_82 e4)) (?v_406 (= ?v_82 e5)) (?v_225 (= ?v_84 e0)) (?v_228 (= ?v_84 e1)) (?v_231 (= ?v_84 e2)) (?v_233 (= ?v_84 e3)) (?v_315 (= ?v_84 e4)) (?v_409 (= ?v_84 e5)) (?v_307 (= ?v_86 e0)) (?v_310 (= ?v_86 e1)) (?v_313 (= ?v_86 e2)) (?v_316 (= ?v_86 e3)) (?v_318 (= ?v_86 e4)) (?v_412 (= ?v_86 e5)) (?v_401 (= ?v_88 e0)) (?v_404 (= ?v_88 e1)) (?v_407 (= ?v_88 e2)) (?v_410 (= ?v_88 e3)) (?v_413 (= ?v_88 e4)) (?v_415 (= ?v_88 e5)) (?v_16 (= ?v_19 e0)) (?v_57 (= ?v_19 e1)) (?v_140 (= ?v_19 e2)) (?v_208 (= ?v_19 e3)) (?v_287 (= ?v_19 e4)) (?v_377 (= ?v_19 e5)) (?v_91 (= ?v_71 e0)) (?v_94 (= ?v_71 e1)) (?v_151 (= ?v_71 e2)) (?v_221 (= ?v_71 e3)) (?v_302 (= ?v_71 e4)) (?v_394 (= ?v_71 e5)) (?v_163 (= ?v_85 e0)) (?v_166 (= ?v_85 e1)) (?v_169 (= ?v_85 e2)) (?v_234 (= ?v_85 e3)) (?v_317 (= ?v_85 e4)) (?v_411 (= ?v_85 e5)) (?v_238 (= ?v_98 e0)) (?v_241 (= ?v_98 e1)) (?v_244 (= ?v_98 e2)) (?v_246 (= ?v_98 e3)) (?v_330 (= ?v_98 e4)) (?v_426 (= ?v_98 e5)) (?v_322 (= ?v_100 e0)) (?v_325 (= ?v_100 e1)) (?v_328 (= ?v_100 e2)) (?v_331 (= ?v_100 e3)) (?v_333 (= ?v_100 e4)) (?v_429 (= ?v_100 e5)) (?v_418 (= ?v_102 e0)) (?v_421 (= ?v_102 e1)) (?v_424 (= ?v_102 e2)) (?v_427 (= ?v_102 e3)) (?v_430 (= ?v_102 e4)) (?v_432 (= ?v_102 e5)) (?v_25 (= ?v_28 e0)) (?v_59 (= ?v_28 e1)) (?v_141 (= ?v_28 e2)) (?v_209 (= ?v_28 e3)) (?v_289 (= ?v_28 e4)) (?v_380 (= ?v_28 e5)) (?v_105 (= ?v_73 e0)) (?v_108 (= ?v_73 e1)) (?v_152 (= ?v_73 e2)) (?v_222 (= ?v_73 e3)) (?v_304 (= ?v_73 e4)) (?v_397 (= ?v_73 e5)) (?v_173 (= ?v_87 e0)) (?v_176 (= ?v_87 e1)) (?v_179 (= ?v_87 e2)) (?v_235 (= ?v_87 e3)) (?v_319 (= ?v_87 e4)) (?v_414 (= ?v_87 e5)) (?v_249 (= ?v_101 e0)) (?v_252 (= ?v_101 e1)) (?v_255 (= ?v_101 e2)) (?v_258 (= ?v_101 e3)) (?v_334 (= ?v_101 e4)) (?v_431 (= ?v_101 e5)) (?v_337 (= ?v_114 e0)) (?v_340 (= ?v_114 e1)) (?v_343 (= ?v_114 e2)) (?v_346 (= ?v_114 e3)) (?v_348 (= ?v_114 e4)) (?v_446 (= ?v_114 e5)) (?v_435 (= ?v_116 e0)) (?v_438 (= ?v_116 e1)) (?v_441 (= ?v_116 e2)) (?v_444 (= ?v_116 e3)) (?v_447 (= ?v_116 e4)) (?v_449 (= ?v_116 e5)) (?v_36 (= ?v_39 e0)) (?v_61 (= ?v_39 e1)) (?v_142 (= ?v_39 e2)) (?v_210 (= ?v_39 e3)) (?v_290 (= ?v_39 e4)) (?v_382 (= ?v_39 e5)) (?v_119 (= ?v_75 e0)) (?v_122 (= ?v_75 e1)) (?v_153 (= ?v_75 e2)) (?v_223 (= ?v_75 e3)) (?v_305 (= ?v_75 e4)) (?v_399 (= ?v_75 e5)) (?v_185 (= ?v_89 e0)) (?v_188 (= ?v_89 e1)) (?v_191 (= ?v_89 e2)) (?v_236 (= ?v_89 e3)) (?v_320 (= ?v_89 e4)) (?v_416 (= ?v_89 e5)) (?v_262 (= ?v_103 e0)) (?v_265 (= ?v_103 e1)) (?v_268 (= ?v_103 e2)) (?v_271 (= ?v_103 e3)) (?v_335 (= ?v_103 e4)) (?v_433 (= ?v_103 e5)) (?v_351 (= ?v_117 e0)) (?v_354 (= ?v_117 e1)) (?v_357 (= ?v_117 e2)) (?v_360 (= ?v_117 e3)) (?v_363 (= ?v_117 e4)) (?v_450 (= ?v_117 e5)) (?v_452 (= ?v_130 e0)) (?v_455 (= ?v_130 e1)) (?v_458 (= ?v_130 e2)) (?v_461 (= ?v_130 e3)) (?v_464 (= ?v_130 e4)) (?v_466 (= ?v_130 e5))) (let ((?v_1 (not ?v_0)) (?v_50 (not ?v_48)) (?v_134 (not ?v_132)) (?v_200 (not ?v_198)) (?v_278 (not ?v_276)) (?v_368 (not ?v_366)) (?v_5 (not ?v_49)) (?v_64 (not ?v_52)) (?v_145 (not ?v_135)) (?v_213 (not ?v_201)) (?v_293 (not ?v_279)) (?v_385 (not ?v_369)) (?v_10 (not ?v_133)) (?v_78 (not ?v_136)) (?v_156 (not ?v_138)) (?v_226 (not ?v_204)) (?v_308 (not ?v_282)) (?v_402 (not ?v_372)) (?v_17 (not ?v_199)) (?v_92 (not ?v_202)) (?v_164 (not ?v_205)) (?v_239 (not ?v_207)) (?v_323 (not ?v_285)) (?v_419 (not ?v_375)) (?v_26 (not ?v_277)) (?v_106 (not ?v_280)) (?v_174 (not ?v_283)) (?v_250 (not ?v_286)) (?v_338 (not ?v_288)) (?v_436 (not ?v_378)) (?v_37 (not ?v_367)) (?v_120 (not ?v_370)) (?v_186 (not ?v_373)) (?v_263 (not ?v_376)) (?v_352 (not ?v_379)) (?v_453 (not ?v_381)) (?v_3 (not ?v_4)) (?v_62 (not ?v_53)) (?v_143 (not ?v_137)) (?v_211 (not ?v_203)) (?v_291 (not ?v_281)) (?v_383 (not ?v_371)) (?v_7 (not ?v_63)) (?v_67 (not ?v_66)) (?v_148 (not ?v_146)) (?v_216 (not ?v_214)) (?v_296 (not ?v_294)) (?v_388 (not ?v_386)) (?v_13 (not ?v_144)) (?v_81 (not ?v_147)) (?v_159 (not ?v_149)) (?v_229 (not ?v_217)) (?v_311 (not ?v_297)) (?v_405 (not ?v_389)) (?v_20 (not ?v_212)) (?v_95 (not ?v_215)) (?v_167 (not ?v_218)) (?v_242 (not ?v_220)) (?v_326 (not ?v_300)) (?v_422 (not ?v_392)) (?v_29 (not ?v_292)) (?v_109 (not ?v_295)) (?v_177 (not ?v_298)) (?v_253 (not ?v_301)) (?v_341 (not ?v_303)) (?v_439 (not ?v_395)) (?v_40 (not ?v_384)) (?v_123 (not ?v_387)) (?v_189 (not ?v_390)) (?v_266 (not ?v_393)) (?v_355 (not ?v_396)) (?v_456 (not ?v_398)) (?v_8 (not ?v_9)) (?v_76 (not ?v_55)) (?v_154 (not ?v_139)) (?v_224 (not ?v_206)) (?v_306 (not ?v_284)) (?v_400 (not ?v_374)) (?v_11 (not ?v_77)) (?v_79 (not ?v_80)) (?v_157 (not ?v_150)) (?v_227 (not ?v_219)) (?v_309 (not ?v_299)) (?v_403 (not ?v_391)) (?v_14 (not ?v_155)) (?v_83 (not ?v_158)) (?v_161 (not ?v_160)) (?v_232 (not ?v_230)) (?v_314 (not ?v_312)) (?v_408 (not ?v_406)) (?v_22 (not ?v_225)) (?v_97 (not ?v_228)) (?v_170 (not ?v_231)) (?v_245 (not ?v_233)) (?v_329 (not ?v_315)) (?v_425 (not ?v_409)) (?v_31 (not ?v_307)) (?v_111 (not ?v_310)) (?v_180 (not ?v_313)) (?v_256 (not ?v_316)) (?v_344 (not ?v_318)) (?v_442 (not ?v_412)) (?v_42 (not ?v_401)) (?v_125 (not ?v_404)) (?v_192 (not ?v_407)) (?v_269 (not ?v_410)) (?v_358 (not ?v_413)) (?v_459 (not ?v_415)) (?v_15 (not ?v_16)) (?v_90 (not ?v_57)) (?v_162 (not ?v_140)) (?v_237 (not ?v_208)) (?v_321 (not ?v_287)) (?v_417 (not ?v_377)) (?v_18 (not ?v_91)) (?v_93 (not ?v_94)) (?v_165 (not ?v_151)) (?v_240 (not ?v_221)) (?v_324 (not ?v_302)) (?v_420 (not ?v_394)) (?v_21 (not ?v_163)) (?v_96 (not ?v_166)) (?v_168 (not ?v_169)) (?v_243 (not ?v_234)) (?v_327 (not ?v_317)) (?v_423 (not ?v_411)) (?v_23 (not ?v_238)) (?v_99 (not ?v_241)) (?v_171 (not ?v_244)) (?v_247 (not ?v_246)) (?v_332 (not ?v_330)) (?v_428 (not ?v_426)) (?v_33 (not ?v_322)) (?v_113 (not ?v_325)) (?v_182 (not ?v_328)) (?v_259 (not ?v_331)) (?v_347 (not ?v_333)) (?v_445 (not ?v_429)) (?v_44 (not ?v_418)) (?v_127 (not ?v_421)) (?v_194 (not ?v_424)) (?v_272 (not ?v_427)) (?v_361 (not ?v_430)) (?v_462 (not ?v_432)) (?v_24 (not ?v_25)) (?v_104 (not ?v_59)) (?v_172 (not ?v_141)) (?v_248 (not ?v_209)) (?v_336 (not ?v_289)) (?v_434 (not ?v_380)) (?v_27 (not ?v_105)) (?v_107 (not ?v_108)) (?v_175 (not ?v_152)) (?v_251 (not ?v_222)) (?v_339 (not ?v_304)) (?v_437 (not ?v_397)) (?v_30 (not ?v_173)) (?v_110 (not ?v_176)) (?v_178 (not ?v_179)) (?v_254 (not ?v_235)) (?v_342 (not ?v_319)) (?v_440 (not ?v_414)) (?v_32 (not ?v_249)) (?v_112 (not ?v_252)) (?v_181 (not ?v_255)) (?v_257 (not ?v_258)) (?v_345 (not ?v_334)) (?v_443 (not ?v_431)) (?v_34 (not ?v_337)) (?v_115 (not ?v_340)) (?v_183 (not ?v_343)) (?v_260 (not ?v_346)) (?v_349 (not ?v_348)) (?v_448 (not ?v_446)) (?v_46 (not ?v_435)) (?v_129 (not ?v_438)) (?v_196 (not ?v_441)) (?v_274 (not ?v_444)) (?v_364 (not ?v_447)) (?v_465 (not ?v_449)) (?v_35 (not ?v_36)) (?v_118 (not ?v_61)) (?v_184 (not ?v_142)) (?v_261 (not ?v_210)) (?v_350 (not ?v_290)) (?v_451 (not ?v_382)) (?v_38 (not ?v_119)) (?v_121 (not ?v_122)) (?v_187 (not ?v_153)) (?v_264 (not ?v_223)) (?v_353 (not ?v_305)) (?v_454 (not ?v_399)) (?v_41 (not ?v_185)) (?v_124 (not ?v_188)) (?v_190 (not ?v_191)) (?v_267 (not ?v_236)) (?v_356 (not ?v_320)) (?v_457 (not ?v_416)) (?v_43 (not ?v_262)) (?v_126 (not ?v_265)) (?v_193 (not ?v_268)) (?v_270 (not ?v_271)) (?v_359 (not ?v_335)) (?v_460 (not ?v_433)) (?v_45 (not ?v_351)) (?v_128 (not ?v_354)) (?v_195 (not ?v_357)) (?v_273 (not ?v_360)) (?v_362 (not ?v_363)) (?v_463 (not ?v_450)) (?v_47 (not ?v_452)) (?v_131 (not ?v_455)) (?v_197 (not ?v_458)) (?v_275 (not ?v_461)) (?v_365 (not ?v_464)) (?v_467 (not ?v_466))) (or (or (or (or (or (and (and (and (and (and (and (and (and (and (and (or ?v_1 (or ?v_0 ?v_1)) (or ?v_5 (or ?v_48 ?v_3))) (or ?v_10 (or ?v_132 ?v_8))) (or ?v_17 (or ?v_198 ?v_15))) (or ?v_26 (or ?v_276 ?v_24))) (or ?v_37 (or ?v_366 ?v_35))) (and (and (and (and (and (or ?v_3 (or ?v_4 ?v_5)) (or ?v_7 (or ?v_53 ?v_7))) (or ?v_13 (or ?v_137 ?v_11))) (or ?v_20 (or ?v_203 ?v_18))) (or ?v_29 (or ?v_281 ?v_27))) (or ?v_40 (or ?v_371 ?v_38)))) (and (and (and (and (and (or ?v_8 (or ?v_9 ?v_10)) (or ?v_11 (or ?v_55 ?v_13))) (or ?v_14 (or ?v_139 ?v_14))) (or ?v_22 (or ?v_206 ?v_21))) (or ?v_31 (or ?v_284 ?v_30))) (or ?v_42 (or ?v_374 ?v_41)))) (and (and (and (and (and (or ?v_15 (or ?v_16 ?v_17)) (or ?v_18 (or ?v_57 ?v_20))) (or ?v_21 (or ?v_140 ?v_22))) (or ?v_23 (or ?v_208 ?v_23))) (or ?v_33 (or ?v_287 ?v_32))) (or ?v_44 (or ?v_377 ?v_43)))) (and (and (and (and (and (or ?v_24 (or ?v_25 ?v_26)) (or ?v_27 (or ?v_59 ?v_29))) (or ?v_30 (or ?v_141 ?v_31))) (or ?v_32 (or ?v_209 ?v_33))) (or ?v_34 (or ?v_289 ?v_34))) (or ?v_46 (or ?v_380 ?v_45)))) (and (and (and (and (and (or ?v_35 (or ?v_36 ?v_37)) (or ?v_38 (or ?v_61 ?v_40))) (or ?v_41 (or ?v_142 ?v_42))) (or ?v_43 (or ?v_210 ?v_44))) (or ?v_45 (or ?v_290 ?v_46))) (or ?v_47 (or ?v_382 ?v_47)))) (and (and (and (and (and (and (and (and (and (and (or ?v_50 (or ?v_49 ?v_50)) (or ?v_64 (or ?v_52 ?v_62))) (or ?v_78 (or ?v_135 ?v_76))) (or ?v_92 (or ?v_201 ?v_90))) (or ?v_106 (or ?v_279 ?v_104))) (or ?v_120 (or ?v_369 ?v_118))) (and (and (and (and (and (or ?v_62 (or ?v_63 ?v_64)) (or ?v_67 (or ?v_66 ?v_67))) (or ?v_81 (or ?v_146 ?v_79))) (or ?v_95 (or ?v_214 ?v_93))) (or ?v_109 (or ?v_294 ?v_107))) (or ?v_123 (or ?v_386 ?v_121)))) (and (and (and (and (and (or ?v_76 (or ?v_77 ?v_78)) (or ?v_79 (or ?v_80 ?v_81))) (or ?v_83 (or ?v_150 ?v_83))) (or ?v_97 (or ?v_219 ?v_96))) (or ?v_111 (or ?v_299 ?v_110))) (or ?v_125 (or ?v_391 ?v_124)))) (and (and (and (and (and (or ?v_90 (or ?v_91 ?v_92)) (or ?v_93 (or ?v_94 ?v_95))) (or ?v_96 (or ?v_151 ?v_97))) (or ?v_99 (or ?v_221 ?v_99))) (or ?v_113 (or ?v_302 ?v_112))) (or ?v_127 (or ?v_394 ?v_126)))) (and (and (and (and (and (or ?v_104 (or ?v_105 ?v_106)) (or ?v_107 (or ?v_108 ?v_109))) (or ?v_110 (or ?v_152 ?v_111))) (or ?v_112 (or ?v_222 ?v_113))) (or ?v_115 (or ?v_304 ?v_115))) (or ?v_129 (or ?v_397 ?v_128)))) (and (and (and (and (and (or ?v_118 (or ?v_119 ?v_120)) (or ?v_121 (or ?v_122 ?v_123))) (or ?v_124 (or ?v_153 ?v_125))) (or ?v_126 (or ?v_223 ?v_127))) (or ?v_128 (or ?v_305 ?v_129))) (or ?v_131 (or ?v_399 ?v_131))))) (and (and (and (and (and (and (and (and (and (and (or ?v_134 (or ?v_133 ?v_134)) (or ?v_145 (or ?v_136 ?v_143))) (or ?v_156 (or ?v_138 ?v_154))) (or ?v_164 (or ?v_204 ?v_162))) (or ?v_174 (or ?v_282 ?v_172))) (or ?v_186 (or ?v_372 ?v_184))) (and (and (and (and (and (or ?v_143 (or ?v_144 ?v_145)) (or ?v_148 (or ?v_147 ?v_148))) (or ?v_159 (or ?v_149 ?v_157))) (or ?v_167 (or ?v_217 ?v_165))) (or ?v_177 (or ?v_297 ?v_175))) (or ?v_189 (or ?v_389 ?v_187)))) (and (and (and (and (and (or ?v_154 (or ?v_155 ?v_156)) (or ?v_157 (or ?v_158 ?v_159))) (or ?v_161 (or ?v_160 ?v_161))) (or ?v_170 (or ?v_230 ?v_168))) (or ?v_180 (or ?v_312 ?v_178))) (or ?v_192 (or ?v_406 ?v_190)))) (and (and (and (and (and (or ?v_162 (or ?v_163 ?v_164)) (or ?v_165 (or ?v_166 ?v_167))) (or ?v_168 (or ?v_169 ?v_170))) (or ?v_171 (or ?v_234 ?v_171))) (or ?v_182 (or ?v_317 ?v_181))) (or ?v_194 (or ?v_411 ?v_193)))) (and (and (and (and (and (or ?v_172 (or ?v_173 ?v_174)) (or ?v_175 (or ?v_176 ?v_177))) (or ?v_178 (or ?v_179 ?v_180))) (or ?v_181 (or ?v_235 ?v_182))) (or ?v_183 (or ?v_319 ?v_183))) (or ?v_196 (or ?v_414 ?v_195)))) (and (and (and (and (and (or ?v_184 (or ?v_185 ?v_186)) (or ?v_187 (or ?v_188 ?v_189))) (or ?v_190 (or ?v_191 ?v_192))) (or ?v_193 (or ?v_236 ?v_194))) (or ?v_195 (or ?v_320 ?v_196))) (or ?v_197 (or ?v_416 ?v_197))))) (and (and (and (and (and (and (and (and (and (and (or ?v_200 (or ?v_199 ?v_200)) (or ?v_213 (or ?v_202 ?v_211))) (or ?v_226 (or ?v_205 ?v_224))) (or ?v_239 (or ?v_207 ?v_237))) (or ?v_250 (or ?v_285 ?v_248))) (or ?v_263 (or ?v_375 ?v_261))) (and (and (and (and (and (or ?v_211 (or ?v_212 ?v_213)) (or ?v_216 (or ?v_215 ?v_216))) (or ?v_229 (or ?v_218 ?v_227))) (or ?v_242 (or ?v_220 ?v_240))) (or ?v_253 (or ?v_300 ?v_251))) (or ?v_266 (or ?v_392 ?v_264)))) (and (and (and (and (and (or ?v_224 (or ?v_225 ?v_226)) (or ?v_227 (or ?v_228 ?v_229))) (or ?v_232 (or ?v_231 ?v_232))) (or ?v_245 (or ?v_233 ?v_243))) (or ?v_256 (or ?v_315 ?v_254))) (or ?v_269 (or ?v_409 ?v_267)))) (and (and (and (and (and (or ?v_237 (or ?v_238 ?v_239)) (or ?v_240 (or ?v_241 ?v_242))) (or ?v_243 (or ?v_244 ?v_245))) (or ?v_247 (or ?v_246 ?v_247))) (or ?v_259 (or ?v_330 ?v_257))) (or ?v_272 (or ?v_426 ?v_270)))) (and (and (and (and (and (or ?v_248 (or ?v_249 ?v_250)) (or ?v_251 (or ?v_252 ?v_253))) (or ?v_254 (or ?v_255 ?v_256))) (or ?v_257 (or ?v_258 ?v_259))) (or ?v_260 (or ?v_334 ?v_260))) (or ?v_274 (or ?v_431 ?v_273)))) (and (and (and (and (and (or ?v_261 (or ?v_262 ?v_263)) (or ?v_264 (or ?v_265 ?v_266))) (or ?v_267 (or ?v_268 ?v_269))) (or ?v_270 (or ?v_271 ?v_272))) (or ?v_273 (or ?v_335 ?v_274))) (or ?v_275 (or ?v_433 ?v_275))))) (and (and (and (and (and (and (and (and (and (and (or ?v_278 (or ?v_277 ?v_278)) (or ?v_293 (or ?v_280 ?v_291))) (or ?v_308 (or ?v_283 ?v_306))) (or ?v_323 (or ?v_286 ?v_321))) (or ?v_338 (or ?v_288 ?v_336))) (or ?v_352 (or ?v_378 ?v_350))) (and (and (and (and (and (or ?v_291 (or ?v_292 ?v_293)) (or ?v_296 (or ?v_295 ?v_296))) (or ?v_311 (or ?v_298 ?v_309))) (or ?v_326 (or ?v_301 ?v_324))) (or ?v_341 (or ?v_303 ?v_339))) (or ?v_355 (or ?v_395 ?v_353)))) (and (and (and (and (and (or ?v_306 (or ?v_307 ?v_308)) (or ?v_309 (or ?v_310 ?v_311))) (or ?v_314 (or ?v_313 ?v_314))) (or ?v_329 (or ?v_316 ?v_327))) (or ?v_344 (or ?v_318 ?v_342))) (or ?v_358 (or ?v_412 ?v_356)))) (and (and (and (and (and (or ?v_321 (or ?v_322 ?v_323)) (or ?v_324 (or ?v_325 ?v_326))) (or ?v_327 (or ?v_328 ?v_329))) (or ?v_332 (or ?v_331 ?v_332))) (or ?v_347 (or ?v_333 ?v_345))) (or ?v_361 (or ?v_429 ?v_359)))) (and (and (and (and (and (or ?v_336 (or ?v_337 ?v_338)) (or ?v_339 (or ?v_340 ?v_341))) (or ?v_342 (or ?v_343 ?v_344))) (or ?v_345 (or ?v_346 ?v_347))) (or ?v_349 (or ?v_348 ?v_349))) (or ?v_364 (or ?v_446 ?v_362)))) (and (and (and (and (and (or ?v_350 (or ?v_351 ?v_352)) (or ?v_353 (or ?v_354 ?v_355))) (or ?v_356 (or ?v_357 ?v_358))) (or ?v_359 (or ?v_360 ?v_361))) (or ?v_362 (or ?v_363 ?v_364))) (or ?v_365 (or ?v_450 ?v_365))))) (and (and (and (and (and (and (and (and (and (and (or ?v_368 (or ?v_367 ?v_368)) (or ?v_385 (or ?v_370 ?v_383))) (or ?v_402 (or ?v_373 ?v_400))) (or ?v_419 (or ?v_376 ?v_417))) (or ?v_436 (or ?v_379 ?v_434))) (or ?v_453 (or ?v_381 ?v_451))) (and (and (and (and (and (or ?v_383 (or ?v_384 ?v_385)) (or ?v_388 (or ?v_387 ?v_388))) (or ?v_405 (or ?v_390 ?v_403))) (or ?v_422 (or ?v_393 ?v_420))) (or ?v_439 (or ?v_396 ?v_437))) (or ?v_456 (or ?v_398 ?v_454)))) (and (and (and (and (and (or ?v_400 (or ?v_401 ?v_402)) (or ?v_403 (or ?v_404 ?v_405))) (or ?v_408 (or ?v_407 ?v_408))) (or ?v_425 (or ?v_410 ?v_423))) (or ?v_442 (or ?v_413 ?v_440))) (or ?v_459 (or ?v_415 ?v_457)))) (and (and (and (and (and (or ?v_417 (or ?v_418 ?v_419)) (or ?v_420 (or ?v_421 ?v_422))) (or ?v_423 (or ?v_424 ?v_425))) (or ?v_428 (or ?v_427 ?v_428))) (or ?v_445 (or ?v_430 ?v_443))) (or ?v_462 (or ?v_432 ?v_460)))) (and (and (and (and (and (or ?v_434 (or ?v_435 ?v_436)) (or ?v_437 (or ?v_438 ?v_439))) (or ?v_440 (or ?v_441 ?v_442))) (or ?v_443 (or ?v_444 ?v_445))) (or ?v_448 (or ?v_447 ?v_448))) (or ?v_465 (or ?v_449 ?v_463)))) (and (and (and (and (and (or ?v_451 (or ?v_452 ?v_453)) (or ?v_454 (or ?v_455 ?v_456))) (or ?v_457 (or ?v_458 ?v_459))) (or ?v_460 (or ?v_461 ?v_462))) (or ?v_463 (or ?v_464 ?v_465))) (or ?v_467 (or ?v_466 ?v_467)))))))))
(assert (let ((?v_6 (op e0 e1)) (?v_12 (op e0 e2)) (?v_18 (op e0 e3)) (?v_24 (op e0 e4)) (?v_30 (op e0 e5)) (?v_1 (op e1 e0)) (?v_13 (op e1 e2)) (?v_19 (op e1 e3)) (?v_25 (op e1 e4)) (?v_31 (op e1 e5)) (?v_2 (op e2 e0)) (?v_8 (op e2 e1)) (?v_20 (op e2 e3)) (?v_26 (op e2 e4)) (?v_32 (op e2 e5)) (?v_3 (op e3 e0)) (?v_9 (op e3 e1)) (?v_15 (op e3 e2)) (?v_27 (op e3 e4)) (?v_33 (op e3 e5)) (?v_4 (op e4 e0)) (?v_10 (op e4 e1)) (?v_16 (op e4 e2)) (?v_22 (op e4 e3)) (?v_34 (op e4 e5)) (?v_5 (op e5 e0)) (?v_11 (op e5 e1)) (?v_17 (op e5 e2)) (?v_23 (op e5 e3)) (?v_29 (op e5 e4)) (?v_0 (not (= (op e0 (op e0 e0)) e0))) (?v_7 (not (= (op e1 (op e1 e1)) e1))) (?v_14 (not (= (op e2 (op e2 e2)) e2))) (?v_21 (not (= (op e3 (op e3 e3)) e3))) (?v_28 (not (= (op e4 (op e4 e4)) e4))) (?v_35 (not (= (op e5 (op e5 e5)) e5)))) (or (or (or (or (or (and (and (and (and (and (or ?v_0 ?v_0) (or (not (= (op e1 ?v_1) e0)) (not (= (op e0 ?v_1) e1)))) (or (not (= (op e2 ?v_2) e0)) (not (= (op e0 ?v_2) e2)))) (or (not (= (op e3 ?v_3) e0)) (not (= (op e0 ?v_3) e3)))) (or (not (= (op e4 ?v_4) e0)) (not (= (op e0 ?v_4) e4)))) (or (not (= (op e5 ?v_5) e0)) (not (= (op e0 ?v_5) e5)))) (and (and (and (and (and (or (not (= (op e0 ?v_6) e1)) (not (= (op e1 ?v_6) e0))) (or ?v_7 ?v_7)) (or (not (= (op e2 ?v_8) e1)) (not (= (op e1 ?v_8) e2)))) (or (not (= (op e3 ?v_9) e1)) (not (= (op e1 ?v_9) e3)))) (or (not (= (op e4 ?v_10) e1)) (not (= (op e1 ?v_10) e4)))) (or (not (= (op e5 ?v_11) e1)) (not (= (op e1 ?v_11) e5))))) (and (and (and (and (and (or (not (= (op e0 ?v_12) e2)) (not (= (op e2 ?v_12) e0))) (or (not (= (op e1 ?v_13) e2)) (not (= (op e2 ?v_13) e1)))) (or ?v_14 ?v_14)) (or (not (= (op e3 ?v_15) e2)) (not (= (op e2 ?v_15) e3)))) (or (not (= (op e4 ?v_16) e2)) (not (= (op e2 ?v_16) e4)))) (or (not (= (op e5 ?v_17) e2)) (not (= (op e2 ?v_17) e5))))) (and (and (and (and (and (or (not (= (op e0 ?v_18) e3)) (not (= (op e3 ?v_18) e0))) (or (not (= (op e1 ?v_19) e3)) (not (= (op e3 ?v_19) e1)))) (or (not (= (op e2 ?v_20) e3)) (not (= (op e3 ?v_20) e2)))) (or ?v_21 ?v_21)) (or (not (= (op e4 ?v_22) e3)) (not (= (op e3 ?v_22) e4)))) (or (not (= (op e5 ?v_23) e3)) (not (= (op e3 ?v_23) e5))))) (and (and (and (and (and (or (not (= (op e0 ?v_24) e4)) (not (= (op e4 ?v_24) e0))) (or (not (= (op e1 ?v_25) e4)) (not (= (op e4 ?v_25) e1)))) (or (not (= (op e2 ?v_26) e4)) (not (= (op e4 ?v_26) e2)))) (or (not (= (op e3 ?v_27) e4)) (not (= (op e4 ?v_27) e3)))) (or ?v_28 ?v_28)) (or (not (= (op e5 ?v_29) e4)) (not (= (op e4 ?v_29) e5))))) (and (and (and (and (and (or (not (= (op e0 ?v_30) e5)) (not (= (op e5 ?v_30) e0))) (or (not (= (op e1 ?v_31) e5)) (not (= (op e5 ?v_31) e1)))) (or (not (= (op e2 ?v_32) e5)) (not (= (op e5 ?v_32) e2)))) (or (not (= (op e3 ?v_33) e5)) (not (= (op e5 ?v_33) e3)))) (or (not (= (op e4 ?v_34) e5)) (not (= (op e5 ?v_34) e4)))) (or ?v_35 ?v_35)))))
(assert (let ((?v_0 (op e0 e0)) (?v_1 (op e0 e1)) (?v_2 (op e0 e2)) (?v_3 (op e0 e3)) (?v_4 (op e0 e4)) (?v_5 (op e0 e5)) (?v_6 (op e1 e0)) (?v_7 (op e1 e1)) (?v_8 (op e1 e2)) (?v_9 (op e1 e3)) (?v_10 (op e1 e4)) (?v_11 (op e1 e5)) (?v_12 (op e2 e0)) (?v_13 (op e2 e1)) (?v_14 (op e2 e2)) (?v_15 (op e2 e3)) (?v_16 (op e2 e4)) (?v_17 (op e2 e5)) (?v_18 (op e3 e0)) (?v_19 (op e3 e1)) (?v_20 (op e3 e2)) (?v_21 (op e3 e3)) (?v_22 (op e3 e4)) (?v_23 (op e3 e5)) (?v_24 (op e4 e0)) (?v_25 (op e4 e1)) (?v_26 (op e4 e2)) (?v_27 (op e4 e3)) (?v_28 (op e4 e4)) (?v_29 (op e4 e5)) (?v_30 (op e5 e0)) (?v_31 (op e5 e1)) (?v_32 (op e5 e2)) (?v_33 (op e5 e3)) (?v_34 (op e5 e4)) (?v_35 (op e5 e5))) (and (and (and (and (and (and (and (and (and (and (or (not (= (op e0 ?v_0) e0)) (= ?v_0 ?v_0)) (or (not (= (op e0 ?v_1) e1)) (= ?v_6 ?v_1))) (or (not (= (op e0 ?v_2) e2)) (= ?v_12 ?v_2))) (or (not (= (op e0 ?v_3) e3)) (= ?v_18 ?v_3))) (or (not (= (op e0 ?v_4) e4)) (= ?v_24 ?v_4))) (or (not (= (op e0 ?v_5) e5)) (= ?v_30 ?v_5))) (and (and (and (and (and (or (not (= (op e1 ?v_6) e0)) (= ?v_1 ?v_6)) (or (not (= (op e1 ?v_7) e1)) (= ?v_7 ?v_7))) (or (not (= (op e1 ?v_8) e2)) (= ?v_13 ?v_8))) (or (not (= (op e1 ?v_9) e3)) (= ?v_19 ?v_9))) (or (not (= (op e1 ?v_10) e4)) (= ?v_25 ?v_10))) (or (not (= (op e1 ?v_11) e5)) (= ?v_31 ?v_11)))) (and (and (and (and (and (or (not (= (op e2 ?v_12) e0)) (= ?v_2 ?v_12)) (or (not (= (op e2 ?v_13) e1)) (= ?v_8 ?v_13))) (or (not (= (op e2 ?v_14) e2)) (= ?v_14 ?v_14))) (or (not (= (op e2 ?v_15) e3)) (= ?v_20 ?v_15))) (or (not (= (op e2 ?v_16) e4)) (= ?v_26 ?v_16))) (or (not (= (op e2 ?v_17) e5)) (= ?v_32 ?v_17)))) (and (and (and (and (and (or (not (= (op e3 ?v_18) e0)) (= ?v_3 ?v_18)) (or (not (= (op e3 ?v_19) e1)) (= ?v_9 ?v_19))) (or (not (= (op e3 ?v_20) e2)) (= ?v_15 ?v_20))) (or (not (= (op e3 ?v_21) e3)) (= ?v_21 ?v_21))) (or (not (= (op e3 ?v_22) e4)) (= ?v_27 ?v_22))) (or (not (= (op e3 ?v_23) e5)) (= ?v_33 ?v_23)))) (and (and (and (and (and (or (not (= (op e4 ?v_24) e0)) (= ?v_4 ?v_24)) (or (not (= (op e4 ?v_25) e1)) (= ?v_10 ?v_25))) (or (not (= (op e4 ?v_26) e2)) (= ?v_16 ?v_26))) (or (not (= (op e4 ?v_27) e3)) (= ?v_22 ?v_27))) (or (not (= (op e4 ?v_28) e4)) (= ?v_28 ?v_28))) (or (not (= (op e4 ?v_29) e5)) (= ?v_34 ?v_29)))) (and (and (and (and (and (or (not (= (op e5 ?v_30) e0)) (= ?v_5 ?v_30)) (or (not (= (op e5 ?v_31) e1)) (= ?v_11 ?v_31))) (or (not (= (op e5 ?v_32) e2)) (= ?v_17 ?v_32))) (or (not (= (op e5 ?v_33) e3)) (= ?v_23 ?v_33))) (or (not (= (op e5 ?v_34) e4)) (= ?v_29 ?v_34))) (or (not (= (op e5 ?v_35) e5)) (= ?v_35 ?v_35))))))
(assert (= unit e0))
(assert (let ((?v_0 (op e0 e0)) (?v_6 (op e0 e1)) (?v_12 (op e0 e2)) (?v_18 (op e0 e3)) (?v_24 (op e0 e4)) (?v_30 (op e0 e5)) (?v_1 (op e1 e0)) (?v_7 (op e1 e1)) (?v_13 (op e1 e2)) (?v_19 (op e1 e3)) (?v_25 (op e1 e4)) (?v_31 (op e1 e5)) (?v_2 (op e2 e0)) (?v_8 (op e2 e1)) (?v_14 (op e2 e2)) (?v_20 (op e2 e3)) (?v_26 (op e2 e4)) (?v_32 (op e2 e5)) (?v_3 (op e3 e0)) (?v_9 (op e3 e1)) (?v_15 (op e3 e2)) (?v_21 (op e3 e3)) (?v_27 (op e3 e4)) (?v_33 (op e3 e5)) (?v_4 (op e4 e0)) (?v_10 (op e4 e1)) (?v_16 (op e4 e2)) (?v_22 (op e4 e3)) (?v_28 (op e4 e4)) (?v_34 (op e4 e5)) (?v_5 (op e5 e0)) (?v_11 (op e5 e1)) (?v_17 (op e5 e2)) (?v_23 (op e5 e3)) (?v_29 (op e5 e4)) (?v_35 (op e5 e5))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_0 ?v_1)) (not (= ?v_0 ?v_2))) (not (= ?v_0 ?v_3))) (not (= ?v_0 ?v_4))) (not (= ?v_0 ?v_5))) (not (= ?v_1 ?v_2))) (not (= ?v_1 ?v_3))) (not (= ?v_1 ?v_4))) (not (= ?v_1 ?v_5))) (not (= ?v_2 ?v_3))) (not (= ?v_2 ?v_4))) (not (= ?v_2 ?v_5))) (not (= ?v_3 ?v_4))) (not (= ?v_3 ?v_5))) (not (= ?v_4 ?v_5))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_6 ?v_7)) (not (= ?v_6 ?v_8))) (not (= ?v_6 ?v_9))) (not (= ?v_6 ?v_10))) (not (= ?v_6 ?v_11))) (not (= ?v_7 ?v_8))) (not (= ?v_7 ?v_9))) (not (= ?v_7 ?v_10))) (not (= ?v_7 ?v_11))) (not (= ?v_8 ?v_9))) (not (= ?v_8 ?v_10))) (not (= ?v_8 ?v_11))) (not (= ?v_9 ?v_10))) (not (= ?v_9 ?v_11))) (not (= ?v_10 ?v_11)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_12 ?v_13)) (not (= ?v_12 ?v_14))) (not (= ?v_12 ?v_15))) (not (= ?v_12 ?v_16))) (not (= ?v_12 ?v_17))) (not (= ?v_13 ?v_14))) (not (= ?v_13 ?v_15))) (not (= ?v_13 ?v_16))) (not (= ?v_13 ?v_17))) (not (= ?v_14 ?v_15))) (not (= ?v_14 ?v_16))) (not (= ?v_14 ?v_17))) (not (= ?v_15 ?v_16))) (not (= ?v_15 ?v_17))) (not (= ?v_16 ?v_17)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_18 ?v_19)) (not (= ?v_18 ?v_20))) (not (= ?v_18 ?v_21))) (not (= ?v_18 ?v_22))) (not (= ?v_18 ?v_23))) (not (= ?v_19 ?v_20))) (not (= ?v_19 ?v_21))) (not (= ?v_19 ?v_22))) (not (= ?v_19 ?v_23))) (not (= ?v_20 ?v_21))) (not (= ?v_20 ?v_22))) (not (= ?v_20 ?v_23))) (not (= ?v_21 ?v_22))) (not (= ?v_21 ?v_23))) (not (= ?v_22 ?v_23)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_24 ?v_25)) (not (= ?v_24 ?v_26))) (not (= ?v_24 ?v_27))) (not (= ?v_24 ?v_28))) (not (= ?v_24 ?v_29))) (not (= ?v_25 ?v_26))) (not (= ?v_25 ?v_27))) (not (= ?v_25 ?v_28))) (not (= ?v_25 ?v_29))) (not (= ?v_26 ?v_27))) (not (= ?v_26 ?v_28))) (not (= ?v_26 ?v_29))) (not (= ?v_27 ?v_28))) (not (= ?v_27 ?v_29))) (not (= ?v_28 ?v_29)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_30 ?v_31)) (not (= ?v_30 ?v_32))) (not (= ?v_30 ?v_33))) (not (= ?v_30 ?v_34))) (not (= ?v_30 ?v_35))) (not (= ?v_31 ?v_32))) (not (= ?v_31 ?v_33))) (not (= ?v_31 ?v_34))) (not (= ?v_31 ?v_35))) (not (= ?v_32 ?v_33))) (not (= ?v_32 ?v_34))) (not (= ?v_32 ?v_35))) (not (= ?v_33 ?v_34))) (not (= ?v_33 ?v_35))) (not (= ?v_34 ?v_35)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_0 ?v_6)) (not (= ?v_0 ?v_12))) (not (= ?v_0 ?v_18))) (not (= ?v_0 ?v_24))) (not (= ?v_0 ?v_30))) (not (= ?v_6 ?v_12))) (not (= ?v_6 ?v_18))) (not (= ?v_6 ?v_24))) (not (= ?v_6 ?v_30))) (not (= ?v_12 ?v_18))) (not (= ?v_12 ?v_24))) (not (= ?v_12 ?v_30))) (not (= ?v_18 ?v_24))) (not (= ?v_18 ?v_30))) (not (= ?v_24 ?v_30))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_1 ?v_7)) (not (= ?v_1 ?v_13))) (not (= ?v_1 ?v_19))) (not (= ?v_1 ?v_25))) (not (= ?v_1 ?v_31))) (not (= ?v_7 ?v_13))) (not (= ?v_7 ?v_19))) (not (= ?v_7 ?v_25))) (not (= ?v_7 ?v_31))) (not (= ?v_13 ?v_19))) (not (= ?v_13 ?v_25))) (not (= ?v_13 ?v_31))) (not (= ?v_19 ?v_25))) (not (= ?v_19 ?v_31))) (not (= ?v_25 ?v_31)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_2 ?v_8)) (not (= ?v_2 ?v_14))) (not (= ?v_2 ?v_20))) (not (= ?v_2 ?v_26))) (not (= ?v_2 ?v_32))) (not (= ?v_8 ?v_14))) (not (= ?v_8 ?v_20))) (not (= ?v_8 ?v_26))) (not (= ?v_8 ?v_32))) (not (= ?v_14 ?v_20))) (not (= ?v_14 ?v_26))) (not (= ?v_14 ?v_32))) (not (= ?v_20 ?v_26))) (not (= ?v_20 ?v_32))) (not (= ?v_26 ?v_32)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_3 ?v_9)) (not (= ?v_3 ?v_15))) (not (= ?v_3 ?v_21))) (not (= ?v_3 ?v_27))) (not (= ?v_3 ?v_33))) (not (= ?v_9 ?v_15))) (not (= ?v_9 ?v_21))) (not (= ?v_9 ?v_27))) (not (= ?v_9 ?v_33))) (not (= ?v_15 ?v_21))) (not (= ?v_15 ?v_27))) (not (= ?v_15 ?v_33))) (not (= ?v_21 ?v_27))) (not (= ?v_21 ?v_33))) (not (= ?v_27 ?v_33)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_4 ?v_10)) (not (= ?v_4 ?v_16))) (not (= ?v_4 ?v_22))) (not (= ?v_4 ?v_28))) (not (= ?v_4 ?v_34))) (not (= ?v_10 ?v_16))) (not (= ?v_10 ?v_22))) (not (= ?v_10 ?v_28))) (not (= ?v_10 ?v_34))) (not (= ?v_16 ?v_22))) (not (= ?v_16 ?v_28))) (not (= ?v_16 ?v_34))) (not (= ?v_22 ?v_28))) (not (= ?v_22 ?v_34))) (not (= ?v_28 ?v_34)))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= ?v_5 ?v_11)) (not (= ?v_5 ?v_17))) (not (= ?v_5 ?v_23))) (not (= ?v_5 ?v_29))) (not (= ?v_5 ?v_35))) (not (= ?v_11 ?v_17))) (not (= ?v_11 ?v_23))) (not (= ?v_11 ?v_29))) (not (= ?v_11 ?v_35))) (not (= ?v_17 ?v_23))) (not (= ?v_17 ?v_29))) (not (= ?v_17 ?v_35))) (not (= ?v_23 ?v_29))) (not (= ?v_23 ?v_35))) (not (= ?v_29 ?v_35)))))))
(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (= e0 e1)) (not (= e0 e2))) (not (= e0 e3))) (not (= e0 e4))) (not (= e0 e5))) (not (= e1 e2))) (not (= e1 e3))) (not (= e1 e4))) (not (= e1 e5))) (not (= e2 e3))) (not (= e2 e4))) (not (= e2 e5))) (not (= e3 e4))) (not (= e3 e5))) (not (= e4 e5))))
(assert (not (and (and (and (and (= e0 (op e4 e3)) (= e2 (op e4 e5))) (= e3 (op e1 e5))) (= e4 (op e3 e5))) (= e5 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e5 e3)) (= e2 (op e5 e4))) (= e3 (op e1 e4))) (= e5 (op e3 e4))) (= e4 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e3 e4)) (= e2 (op e3 e5))) (= e4 (op e1 e5))) (= e3 (op e4 e5))) (= e5 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e5 e4)) (= e2 (op e5 e3))) (= e4 (op e1 e3))) (= e5 (op e4 e3))) (= e3 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e3 e5)) (= e2 (op e3 e4))) (= e5 (op e1 e4))) (= e3 (op e5 e4))) (= e4 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e4 e5)) (= e2 (op e4 e3))) (= e5 (op e1 e3))) (= e4 (op e5 e3))) (= e3 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e4 e2)) (= e3 (op e4 e5))) (= e2 (op e1 e5))) (= e4 (op e2 e5))) (= e5 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e5 e2)) (= e3 (op e5 e4))) (= e2 (op e1 e4))) (= e5 (op e2 e4))) (= e4 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e2 e4)) (= e3 (op e2 e5))) (= e4 (op e1 e5))) (= e2 (op e4 e5))) (= e5 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e5 e4)) (= e3 (op e5 e2))) (= e4 (op e1 e2))) (= e5 (op e4 e2))) (= e2 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e2 e5)) (= e3 (op e2 e4))) (= e5 (op e1 e4))) (= e2 (op e5 e4))) (= e4 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e4 e5)) (= e3 (op e4 e2))) (= e5 (op e1 e2))) (= e4 (op e5 e2))) (= e2 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e3 e2)) (= e4 (op e3 e5))) (= e2 (op e1 e5))) (= e3 (op e2 e5))) (= e5 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e5 e2)) (= e4 (op e5 e3))) (= e2 (op e1 e3))) (= e5 (op e2 e3))) (= e3 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e2 e3)) (= e4 (op e2 e5))) (= e3 (op e1 e5))) (= e2 (op e3 e5))) (= e5 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e5 e3)) (= e4 (op e5 e2))) (= e3 (op e1 e2))) (= e5 (op e3 e2))) (= e2 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e2 e5)) (= e4 (op e2 e3))) (= e5 (op e1 e3))) (= e2 (op e5 e3))) (= e3 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e3 e5)) (= e4 (op e3 e2))) (= e5 (op e1 e2))) (= e3 (op e5 e2))) (= e2 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e3 e2)) (= e5 (op e3 e4))) (= e2 (op e1 e4))) (= e3 (op e2 e4))) (= e4 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e4 e2)) (= e5 (op e4 e3))) (= e2 (op e1 e3))) (= e4 (op e2 e3))) (= e3 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e2 e3)) (= e5 (op e2 e4))) (= e3 (op e1 e4))) (= e2 (op e3 e4))) (= e4 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e4 e3)) (= e5 (op e4 e2))) (= e3 (op e1 e2))) (= e4 (op e3 e2))) (= e2 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e2 e4)) (= e5 (op e2 e3))) (= e4 (op e1 e3))) (= e2 (op e4 e3))) (= e3 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e3 e4)) (= e5 (op e3 e2))) (= e4 (op e1 e2))) (= e3 (op e4 e2))) (= e2 (op e1 e1)))))
(assert (not (and (and (and (and (= e2 (op e4 e3)) (= e0 (op e4 e5))) (= e3 (op e1 e5))) (= e4 (op e3 e5))) (= e5 (op e1 e1)))))
(assert (not (and (and (and (and (= e2 (op e5 e3)) (= e0 (op e5 e4))) (= e3 (op e1 e4))) (= e5 (op e3 e4))) (= e4 (op e1 e1)))))
(assert (not (and (and (and (and (= e2 (op e3 e4)) (= e0 (op e3 e5))) (= e4 (op e1 e5))) (= e3 (op e4 e5))) (= e5 (op e1 e1)))))
(assert (not (and (and (and (and (= e2 (op e5 e4)) (= e0 (op e5 e3))) (= e4 (op e1 e3))) (= e5 (op e4 e3))) (= e3 (op e1 e1)))))
(assert (not (and (and (and (and (= e2 (op e3 e5)) (= e0 (op e3 e4))) (= e5 (op e1 e4))) (= e3 (op e5 e4))) (= e4 (op e1 e1)))))
(assert (not (and (and (and (and (= e2 (op e4 e5)) (= e0 (op e4 e3))) (= e5 (op e1 e3))) (= e4 (op e5 e3))) (= e3 (op e1 e1)))))
(assert (not (and (and (and (and (= e3 (op e4 e2)) (= e0 (op e4 e5))) (= e2 (op e1 e5))) (= e4 (op e2 e5))) (= e5 (op e1 e1)))))
(assert (not (and (and (and (and (= e3 (op e5 e2)) (= e0 (op e5 e4))) (= e2 (op e1 e4))) (= e5 (op e2 e4))) (= e4 (op e1 e1)))))
(assert (not (and (and (and (and (= e3 (op e2 e4)) (= e0 (op e2 e5))) (= e4 (op e1 e5))) (= e2 (op e4 e5))) (= e5 (op e1 e1)))))
(assert (not (and (and (and (and (= e3 (op e5 e4)) (= e0 (op e5 e2))) (= e4 (op e1 e2))) (= e5 (op e4 e2))) (= e2 (op e1 e1)))))
(assert (not (and (and (and (and (= e3 (op e2 e5)) (= e0 (op e2 e4))) (= e5 (op e1 e4))) (= e2 (op e5 e4))) (= e4 (op e1 e1)))))
(assert (not (and (and (and (and (= e3 (op e4 e5)) (= e0 (op e4 e2))) (= e5 (op e1 e2))) (= e4 (op e5 e2))) (= e2 (op e1 e1)))))
(assert (not (and (and (and (and (= e4 (op e3 e2)) (= e0 (op e3 e5))) (= e2 (op e1 e5))) (= e3 (op e2 e5))) (= e5 (op e1 e1)))))
(assert (not (and (and (and (and (= e4 (op e5 e2)) (= e0 (op e5 e3))) (= e2 (op e1 e3))) (= e5 (op e2 e3))) (= e3 (op e1 e1)))))
(assert (not (and (and (and (and (= e4 (op e2 e3)) (= e0 (op e2 e5))) (= e3 (op e1 e5))) (= e2 (op e3 e5))) (= e5 (op e1 e1)))))
(assert (not (and (and (and (and (= e4 (op e5 e3)) (= e0 (op e5 e2))) (= e3 (op e1 e2))) (= e5 (op e3 e2))) (= e2 (op e1 e1)))))
(assert (not (and (and (and (and (= e4 (op e2 e5)) (= e0 (op e2 e3))) (= e5 (op e1 e3))) (= e2 (op e5 e3))) (= e3 (op e1 e1)))))
(assert (not (and (and (and (and (= e4 (op e3 e5)) (= e0 (op e3 e2))) (= e5 (op e1 e2))) (= e3 (op e5 e2))) (= e2 (op e1 e1)))))
(assert (not (and (and (and (and (= e5 (op e3 e2)) (= e0 (op e3 e4))) (= e2 (op e1 e4))) (= e3 (op e2 e4))) (= e4 (op e1 e1)))))
(assert (not (and (and (and (and (= e5 (op e4 e2)) (= e0 (op e4 e3))) (= e2 (op e1 e3))) (= e4 (op e2 e3))) (= e3 (op e1 e1)))))
(assert (not (and (and (and (and (= e5 (op e2 e3)) (= e0 (op e2 e4))) (= e3 (op e1 e4))) (= e2 (op e3 e4))) (= e4 (op e1 e1)))))
(assert (not (and (and (and (and (= e5 (op e4 e3)) (= e0 (op e4 e2))) (= e3 (op e1 e2))) (= e4 (op e3 e2))) (= e2 (op e1 e1)))))
(assert (not (and (and (and (and (= e5 (op e2 e4)) (= e0 (op e2 e3))) (= e4 (op e1 e3))) (= e2 (op e4 e3))) (= e3 (op e1 e1)))))
(assert (not (and (and (and (and (= e5 (op e3 e4)) (= e0 (op e3 e2))) (= e4 (op e1 e2))) (= e3 (op e4 e2))) (= e2 (op e1 e1)))))
(assert (not (and (and (and (and (= e0 (op e4 e3)) (= e1 (op e4 e5))) (= e3 (op e2 e5))) (= e4 (op e3 e5))) (= e5 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e5 e3)) (= e1 (op e5 e4))) (= e3 (op e2 e4))) (= e5 (op e3 e4))) (= e4 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e3 e4)) (= e1 (op e3 e5))) (= e4 (op e2 e5))) (= e3 (op e4 e5))) (= e5 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e5 e4)) (= e1 (op e5 e3))) (= e4 (op e2 e3))) (= e5 (op e4 e3))) (= e3 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e3 e5)) (= e1 (op e3 e4))) (= e5 (op e2 e4))) (= e3 (op e5 e4))) (= e4 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e4 e5)) (= e1 (op e4 e3))) (= e5 (op e2 e3))) (= e4 (op e5 e3))) (= e3 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e4 e1)) (= e3 (op e4 e5))) (= e1 (op e2 e5))) (= e4 (op e1 e5))) (= e5 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e5 e1)) (= e3 (op e5 e4))) (= e1 (op e2 e4))) (= e5 (op e1 e4))) (= e4 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e1 e4)) (= e3 (op e1 e5))) (= e4 (op e2 e5))) (= e1 (op e4 e5))) (= e5 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e5 e4)) (= e3 (op e5 e1))) (= e4 (op e2 e1))) (= e5 (op e4 e1))) (= e1 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e1 e5)) (= e3 (op e1 e4))) (= e5 (op e2 e4))) (= e1 (op e5 e4))) (= e4 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e4 e5)) (= e3 (op e4 e1))) (= e5 (op e2 e1))) (= e4 (op e5 e1))) (= e1 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e3 e1)) (= e4 (op e3 e5))) (= e1 (op e2 e5))) (= e3 (op e1 e5))) (= e5 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e5 e1)) (= e4 (op e5 e3))) (= e1 (op e2 e3))) (= e5 (op e1 e3))) (= e3 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e1 e3)) (= e4 (op e1 e5))) (= e3 (op e2 e5))) (= e1 (op e3 e5))) (= e5 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e5 e3)) (= e4 (op e5 e1))) (= e3 (op e2 e1))) (= e5 (op e3 e1))) (= e1 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e1 e5)) (= e4 (op e1 e3))) (= e5 (op e2 e3))) (= e1 (op e5 e3))) (= e3 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e3 e5)) (= e4 (op e3 e1))) (= e5 (op e2 e1))) (= e3 (op e5 e1))) (= e1 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e3 e1)) (= e5 (op e3 e4))) (= e1 (op e2 e4))) (= e3 (op e1 e4))) (= e4 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e4 e1)) (= e5 (op e4 e3))) (= e1 (op e2 e3))) (= e4 (op e1 e3))) (= e3 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e1 e3)) (= e5 (op e1 e4))) (= e3 (op e2 e4))) (= e1 (op e3 e4))) (= e4 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e4 e3)) (= e5 (op e4 e1))) (= e3 (op e2 e1))) (= e4 (op e3 e1))) (= e1 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e1 e4)) (= e5 (op e1 e3))) (= e4 (op e2 e3))) (= e1 (op e4 e3))) (= e3 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e3 e4)) (= e5 (op e3 e1))) (= e4 (op e2 e1))) (= e3 (op e4 e1))) (= e1 (op e2 e2)))))
(assert (not (and (and (and (and (= e1 (op e4 e3)) (= e0 (op e4 e5))) (= e3 (op e2 e5))) (= e4 (op e3 e5))) (= e5 (op e2 e2)))))
(assert (not (and (and (and (and (= e1 (op e5 e3)) (= e0 (op e5 e4))) (= e3 (op e2 e4))) (= e5 (op e3 e4))) (= e4 (op e2 e2)))))
(assert (not (and (and (and (and (= e1 (op e3 e4)) (= e0 (op e3 e5))) (= e4 (op e2 e5))) (= e3 (op e4 e5))) (= e5 (op e2 e2)))))
(assert (not (and (and (and (and (= e1 (op e5 e4)) (= e0 (op e5 e3))) (= e4 (op e2 e3))) (= e5 (op e4 e3))) (= e3 (op e2 e2)))))
(assert (not (and (and (and (and (= e1 (op e3 e5)) (= e0 (op e3 e4))) (= e5 (op e2 e4))) (= e3 (op e5 e4))) (= e4 (op e2 e2)))))
(assert (not (and (and (and (and (= e1 (op e4 e5)) (= e0 (op e4 e3))) (= e5 (op e2 e3))) (= e4 (op e5 e3))) (= e3 (op e2 e2)))))
(assert (not (and (and (and (and (= e3 (op e4 e1)) (= e0 (op e4 e5))) (= e1 (op e2 e5))) (= e4 (op e1 e5))) (= e5 (op e2 e2)))))
(assert (not (and (and (and (and (= e3 (op e5 e1)) (= e0 (op e5 e4))) (= e1 (op e2 e4))) (= e5 (op e1 e4))) (= e4 (op e2 e2)))))
(assert (not (and (and (and (and (= e3 (op e1 e4)) (= e0 (op e1 e5))) (= e4 (op e2 e5))) (= e1 (op e4 e5))) (= e5 (op e2 e2)))))
(assert (not (and (and (and (and (= e3 (op e5 e4)) (= e0 (op e5 e1))) (= e4 (op e2 e1))) (= e5 (op e4 e1))) (= e1 (op e2 e2)))))
(assert (not (and (and (and (and (= e3 (op e1 e5)) (= e0 (op e1 e4))) (= e5 (op e2 e4))) (= e1 (op e5 e4))) (= e4 (op e2 e2)))))
(assert (not (and (and (and (and (= e3 (op e4 e5)) (= e0 (op e4 e1))) (= e5 (op e2 e1))) (= e4 (op e5 e1))) (= e1 (op e2 e2)))))
(assert (not (and (and (and (and (= e4 (op e3 e1)) (= e0 (op e3 e5))) (= e1 (op e2 e5))) (= e3 (op e1 e5))) (= e5 (op e2 e2)))))
(assert (not (and (and (and (and (= e4 (op e5 e1)) (= e0 (op e5 e3))) (= e1 (op e2 e3))) (= e5 (op e1 e3))) (= e3 (op e2 e2)))))
(assert (not (and (and (and (and (= e4 (op e1 e3)) (= e0 (op e1 e5))) (= e3 (op e2 e5))) (= e1 (op e3 e5))) (= e5 (op e2 e2)))))
(assert (not (and (and (and (and (= e4 (op e5 e3)) (= e0 (op e5 e1))) (= e3 (op e2 e1))) (= e5 (op e3 e1))) (= e1 (op e2 e2)))))
(assert (not (and (and (and (and (= e4 (op e1 e5)) (= e0 (op e1 e3))) (= e5 (op e2 e3))) (= e1 (op e5 e3))) (= e3 (op e2 e2)))))
(assert (not (and (and (and (and (= e4 (op e3 e5)) (= e0 (op e3 e1))) (= e5 (op e2 e1))) (= e3 (op e5 e1))) (= e1 (op e2 e2)))))
(assert (not (and (and (and (and (= e5 (op e3 e1)) (= e0 (op e3 e4))) (= e1 (op e2 e4))) (= e3 (op e1 e4))) (= e4 (op e2 e2)))))
(assert (not (and (and (and (and (= e5 (op e4 e1)) (= e0 (op e4 e3))) (= e1 (op e2 e3))) (= e4 (op e1 e3))) (= e3 (op e2 e2)))))
(assert (not (and (and (and (and (= e5 (op e1 e3)) (= e0 (op e1 e4))) (= e3 (op e2 e4))) (= e1 (op e3 e4))) (= e4 (op e2 e2)))))
(assert (not (and (and (and (and (= e5 (op e4 e3)) (= e0 (op e4 e1))) (= e3 (op e2 e1))) (= e4 (op e3 e1))) (= e1 (op e2 e2)))))
(assert (not (and (and (and (and (= e5 (op e1 e4)) (= e0 (op e1 e3))) (= e4 (op e2 e3))) (= e1 (op e4 e3))) (= e3 (op e2 e2)))))
(assert (not (and (and (and (and (= e5 (op e3 e4)) (= e0 (op e3 e1))) (= e4 (op e2 e1))) (= e3 (op e4 e1))) (= e1 (op e2 e2)))))
(assert (not (and (and (and (and (= e0 (op e4 e2)) (= e1 (op e4 e5))) (= e2 (op e3 e5))) (= e4 (op e2 e5))) (= e5 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e5 e2)) (= e1 (op e5 e4))) (= e2 (op e3 e4))) (= e5 (op e2 e4))) (= e4 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e2 e4)) (= e1 (op e2 e5))) (= e4 (op e3 e5))) (= e2 (op e4 e5))) (= e5 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e5 e4)) (= e1 (op e5 e2))) (= e4 (op e3 e2))) (= e5 (op e4 e2))) (= e2 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e2 e5)) (= e1 (op e2 e4))) (= e5 (op e3 e4))) (= e2 (op e5 e4))) (= e4 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e4 e5)) (= e1 (op e4 e2))) (= e5 (op e3 e2))) (= e4 (op e5 e2))) (= e2 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e4 e1)) (= e2 (op e4 e5))) (= e1 (op e3 e5))) (= e4 (op e1 e5))) (= e5 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e5 e1)) (= e2 (op e5 e4))) (= e1 (op e3 e4))) (= e5 (op e1 e4))) (= e4 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e1 e4)) (= e2 (op e1 e5))) (= e4 (op e3 e5))) (= e1 (op e4 e5))) (= e5 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e5 e4)) (= e2 (op e5 e1))) (= e4 (op e3 e1))) (= e5 (op e4 e1))) (= e1 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e1 e5)) (= e2 (op e1 e4))) (= e5 (op e3 e4))) (= e1 (op e5 e4))) (= e4 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e4 e5)) (= e2 (op e4 e1))) (= e5 (op e3 e1))) (= e4 (op e5 e1))) (= e1 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e2 e1)) (= e4 (op e2 e5))) (= e1 (op e3 e5))) (= e2 (op e1 e5))) (= e5 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e5 e1)) (= e4 (op e5 e2))) (= e1 (op e3 e2))) (= e5 (op e1 e2))) (= e2 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e1 e2)) (= e4 (op e1 e5))) (= e2 (op e3 e5))) (= e1 (op e2 e5))) (= e5 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e5 e2)) (= e4 (op e5 e1))) (= e2 (op e3 e1))) (= e5 (op e2 e1))) (= e1 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e1 e5)) (= e4 (op e1 e2))) (= e5 (op e3 e2))) (= e1 (op e5 e2))) (= e2 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e2 e5)) (= e4 (op e2 e1))) (= e5 (op e3 e1))) (= e2 (op e5 e1))) (= e1 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e2 e1)) (= e5 (op e2 e4))) (= e1 (op e3 e4))) (= e2 (op e1 e4))) (= e4 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e4 e1)) (= e5 (op e4 e2))) (= e1 (op e3 e2))) (= e4 (op e1 e2))) (= e2 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e1 e2)) (= e5 (op e1 e4))) (= e2 (op e3 e4))) (= e1 (op e2 e4))) (= e4 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e4 e2)) (= e5 (op e4 e1))) (= e2 (op e3 e1))) (= e4 (op e2 e1))) (= e1 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e1 e4)) (= e5 (op e1 e2))) (= e4 (op e3 e2))) (= e1 (op e4 e2))) (= e2 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e2 e4)) (= e5 (op e2 e1))) (= e4 (op e3 e1))) (= e2 (op e4 e1))) (= e1 (op e3 e3)))))
(assert (not (and (and (and (and (= e1 (op e4 e2)) (= e0 (op e4 e5))) (= e2 (op e3 e5))) (= e4 (op e2 e5))) (= e5 (op e3 e3)))))
(assert (not (and (and (and (and (= e1 (op e5 e2)) (= e0 (op e5 e4))) (= e2 (op e3 e4))) (= e5 (op e2 e4))) (= e4 (op e3 e3)))))
(assert (not (and (and (and (and (= e1 (op e2 e4)) (= e0 (op e2 e5))) (= e4 (op e3 e5))) (= e2 (op e4 e5))) (= e5 (op e3 e3)))))
(assert (not (and (and (and (and (= e1 (op e5 e4)) (= e0 (op e5 e2))) (= e4 (op e3 e2))) (= e5 (op e4 e2))) (= e2 (op e3 e3)))))
(assert (not (and (and (and (and (= e1 (op e2 e5)) (= e0 (op e2 e4))) (= e5 (op e3 e4))) (= e2 (op e5 e4))) (= e4 (op e3 e3)))))
(assert (not (and (and (and (and (= e1 (op e4 e5)) (= e0 (op e4 e2))) (= e5 (op e3 e2))) (= e4 (op e5 e2))) (= e2 (op e3 e3)))))
(assert (not (and (and (and (and (= e2 (op e4 e1)) (= e0 (op e4 e5))) (= e1 (op e3 e5))) (= e4 (op e1 e5))) (= e5 (op e3 e3)))))
(assert (not (and (and (and (and (= e2 (op e5 e1)) (= e0 (op e5 e4))) (= e1 (op e3 e4))) (= e5 (op e1 e4))) (= e4 (op e3 e3)))))
(assert (not (and (and (and (and (= e2 (op e1 e4)) (= e0 (op e1 e5))) (= e4 (op e3 e5))) (= e1 (op e4 e5))) (= e5 (op e3 e3)))))
(assert (not (and (and (and (and (= e2 (op e5 e4)) (= e0 (op e5 e1))) (= e4 (op e3 e1))) (= e5 (op e4 e1))) (= e1 (op e3 e3)))))
(assert (not (and (and (and (and (= e2 (op e1 e5)) (= e0 (op e1 e4))) (= e5 (op e3 e4))) (= e1 (op e5 e4))) (= e4 (op e3 e3)))))
(assert (not (and (and (and (and (= e2 (op e4 e5)) (= e0 (op e4 e1))) (= e5 (op e3 e1))) (= e4 (op e5 e1))) (= e1 (op e3 e3)))))
(assert (not (and (and (and (and (= e4 (op e2 e1)) (= e0 (op e2 e5))) (= e1 (op e3 e5))) (= e2 (op e1 e5))) (= e5 (op e3 e3)))))
(assert (not (and (and (and (and (= e4 (op e5 e1)) (= e0 (op e5 e2))) (= e1 (op e3 e2))) (= e5 (op e1 e2))) (= e2 (op e3 e3)))))
(assert (not (and (and (and (and (= e4 (op e1 e2)) (= e0 (op e1 e5))) (= e2 (op e3 e5))) (= e1 (op e2 e5))) (= e5 (op e3 e3)))))
(assert (not (and (and (and (and (= e4 (op e5 e2)) (= e0 (op e5 e1))) (= e2 (op e3 e1))) (= e5 (op e2 e1))) (= e1 (op e3 e3)))))
(assert (not (and (and (and (and (= e4 (op e1 e5)) (= e0 (op e1 e2))) (= e5 (op e3 e2))) (= e1 (op e5 e2))) (= e2 (op e3 e3)))))
(assert (not (and (and (and (and (= e4 (op e2 e5)) (= e0 (op e2 e1))) (= e5 (op e3 e1))) (= e2 (op e5 e1))) (= e1 (op e3 e3)))))
(assert (not (and (and (and (and (= e5 (op e2 e1)) (= e0 (op e2 e4))) (= e1 (op e3 e4))) (= e2 (op e1 e4))) (= e4 (op e3 e3)))))
(assert (not (and (and (and (and (= e5 (op e4 e1)) (= e0 (op e4 e2))) (= e1 (op e3 e2))) (= e4 (op e1 e2))) (= e2 (op e3 e3)))))
(assert (not (and (and (and (and (= e5 (op e1 e2)) (= e0 (op e1 e4))) (= e2 (op e3 e4))) (= e1 (op e2 e4))) (= e4 (op e3 e3)))))
(assert (not (and (and (and (and (= e5 (op e4 e2)) (= e0 (op e4 e1))) (= e2 (op e3 e1))) (= e4 (op e2 e1))) (= e1 (op e3 e3)))))
(assert (not (and (and (and (and (= e5 (op e1 e4)) (= e0 (op e1 e2))) (= e4 (op e3 e2))) (= e1 (op e4 e2))) (= e2 (op e3 e3)))))
(assert (not (and (and (and (and (= e5 (op e2 e4)) (= e0 (op e2 e1))) (= e4 (op e3 e1))) (= e2 (op e4 e1))) (= e1 (op e3 e3)))))
(assert (not (and (and (and (and (= e0 (op e3 e2)) (= e1 (op e3 e5))) (= e2 (op e4 e5))) (= e3 (op e2 e5))) (= e5 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e5 e2)) (= e1 (op e5 e3))) (= e2 (op e4 e3))) (= e5 (op e2 e3))) (= e3 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e2 e3)) (= e1 (op e2 e5))) (= e3 (op e4 e5))) (= e2 (op e3 e5))) (= e5 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e5 e3)) (= e1 (op e5 e2))) (= e3 (op e4 e2))) (= e5 (op e3 e2))) (= e2 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e2 e5)) (= e1 (op e2 e3))) (= e5 (op e4 e3))) (= e2 (op e5 e3))) (= e3 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e3 e5)) (= e1 (op e3 e2))) (= e5 (op e4 e2))) (= e3 (op e5 e2))) (= e2 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e3 e1)) (= e2 (op e3 e5))) (= e1 (op e4 e5))) (= e3 (op e1 e5))) (= e5 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e5 e1)) (= e2 (op e5 e3))) (= e1 (op e4 e3))) (= e5 (op e1 e3))) (= e3 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e1 e3)) (= e2 (op e1 e5))) (= e3 (op e4 e5))) (= e1 (op e3 e5))) (= e5 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e5 e3)) (= e2 (op e5 e1))) (= e3 (op e4 e1))) (= e5 (op e3 e1))) (= e1 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e1 e5)) (= e2 (op e1 e3))) (= e5 (op e4 e3))) (= e1 (op e5 e3))) (= e3 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e3 e5)) (= e2 (op e3 e1))) (= e5 (op e4 e1))) (= e3 (op e5 e1))) (= e1 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e2 e1)) (= e3 (op e2 e5))) (= e1 (op e4 e5))) (= e2 (op e1 e5))) (= e5 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e5 e1)) (= e3 (op e5 e2))) (= e1 (op e4 e2))) (= e5 (op e1 e2))) (= e2 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e1 e2)) (= e3 (op e1 e5))) (= e2 (op e4 e5))) (= e1 (op e2 e5))) (= e5 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e5 e2)) (= e3 (op e5 e1))) (= e2 (op e4 e1))) (= e5 (op e2 e1))) (= e1 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e1 e5)) (= e3 (op e1 e2))) (= e5 (op e4 e2))) (= e1 (op e5 e2))) (= e2 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e2 e5)) (= e3 (op e2 e1))) (= e5 (op e4 e1))) (= e2 (op e5 e1))) (= e1 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e2 e1)) (= e5 (op e2 e3))) (= e1 (op e4 e3))) (= e2 (op e1 e3))) (= e3 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e3 e1)) (= e5 (op e3 e2))) (= e1 (op e4 e2))) (= e3 (op e1 e2))) (= e2 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e1 e2)) (= e5 (op e1 e3))) (= e2 (op e4 e3))) (= e1 (op e2 e3))) (= e3 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e3 e2)) (= e5 (op e3 e1))) (= e2 (op e4 e1))) (= e3 (op e2 e1))) (= e1 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e1 e3)) (= e5 (op e1 e2))) (= e3 (op e4 e2))) (= e1 (op e3 e2))) (= e2 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e2 e3)) (= e5 (op e2 e1))) (= e3 (op e4 e1))) (= e2 (op e3 e1))) (= e1 (op e4 e4)))))
(assert (not (and (and (and (and (= e1 (op e3 e2)) (= e0 (op e3 e5))) (= e2 (op e4 e5))) (= e3 (op e2 e5))) (= e5 (op e4 e4)))))
(assert (not (and (and (and (and (= e1 (op e5 e2)) (= e0 (op e5 e3))) (= e2 (op e4 e3))) (= e5 (op e2 e3))) (= e3 (op e4 e4)))))
(assert (not (and (and (and (and (= e1 (op e2 e3)) (= e0 (op e2 e5))) (= e3 (op e4 e5))) (= e2 (op e3 e5))) (= e5 (op e4 e4)))))
(assert (not (and (and (and (and (= e1 (op e5 e3)) (= e0 (op e5 e2))) (= e3 (op e4 e2))) (= e5 (op e3 e2))) (= e2 (op e4 e4)))))
(assert (not (and (and (and (and (= e1 (op e2 e5)) (= e0 (op e2 e3))) (= e5 (op e4 e3))) (= e2 (op e5 e3))) (= e3 (op e4 e4)))))
(assert (not (and (and (and (and (= e1 (op e3 e5)) (= e0 (op e3 e2))) (= e5 (op e4 e2))) (= e3 (op e5 e2))) (= e2 (op e4 e4)))))
(assert (not (and (and (and (and (= e2 (op e3 e1)) (= e0 (op e3 e5))) (= e1 (op e4 e5))) (= e3 (op e1 e5))) (= e5 (op e4 e4)))))
(assert (not (and (and (and (and (= e2 (op e5 e1)) (= e0 (op e5 e3))) (= e1 (op e4 e3))) (= e5 (op e1 e3))) (= e3 (op e4 e4)))))
(assert (not (and (and (and (and (= e2 (op e1 e3)) (= e0 (op e1 e5))) (= e3 (op e4 e5))) (= e1 (op e3 e5))) (= e5 (op e4 e4)))))
(assert (not (and (and (and (and (= e2 (op e5 e3)) (= e0 (op e5 e1))) (= e3 (op e4 e1))) (= e5 (op e3 e1))) (= e1 (op e4 e4)))))
(assert (not (and (and (and (and (= e2 (op e1 e5)) (= e0 (op e1 e3))) (= e5 (op e4 e3))) (= e1 (op e5 e3))) (= e3 (op e4 e4)))))
(assert (not (and (and (and (and (= e2 (op e3 e5)) (= e0 (op e3 e1))) (= e5 (op e4 e1))) (= e3 (op e5 e1))) (= e1 (op e4 e4)))))
(assert (not (and (and (and (and (= e3 (op e2 e1)) (= e0 (op e2 e5))) (= e1 (op e4 e5))) (= e2 (op e1 e5))) (= e5 (op e4 e4)))))
(assert (not (and (and (and (and (= e3 (op e5 e1)) (= e0 (op e5 e2))) (= e1 (op e4 e2))) (= e5 (op e1 e2))) (= e2 (op e4 e4)))))
(assert (not (and (and (and (and (= e3 (op e1 e2)) (= e0 (op e1 e5))) (= e2 (op e4 e5))) (= e1 (op e2 e5))) (= e5 (op e4 e4)))))
(assert (not (and (and (and (and (= e3 (op e5 e2)) (= e0 (op e5 e1))) (= e2 (op e4 e1))) (= e5 (op e2 e1))) (= e1 (op e4 e4)))))
(assert (not (and (and (and (and (= e3 (op e1 e5)) (= e0 (op e1 e2))) (= e5 (op e4 e2))) (= e1 (op e5 e2))) (= e2 (op e4 e4)))))
(assert (not (and (and (and (and (= e3 (op e2 e5)) (= e0 (op e2 e1))) (= e5 (op e4 e1))) (= e2 (op e5 e1))) (= e1 (op e4 e4)))))
(assert (not (and (and (and (and (= e5 (op e2 e1)) (= e0 (op e2 e3))) (= e1 (op e4 e3))) (= e2 (op e1 e3))) (= e3 (op e4 e4)))))
(assert (not (and (and (and (and (= e5 (op e3 e1)) (= e0 (op e3 e2))) (= e1 (op e4 e2))) (= e3 (op e1 e2))) (= e2 (op e4 e4)))))
(assert (not (and (and (and (and (= e5 (op e1 e2)) (= e0 (op e1 e3))) (= e2 (op e4 e3))) (= e1 (op e2 e3))) (= e3 (op e4 e4)))))
(assert (not (and (and (and (and (= e5 (op e3 e2)) (= e0 (op e3 e1))) (= e2 (op e4 e1))) (= e3 (op e2 e1))) (= e1 (op e4 e4)))))
(assert (not (and (and (and (and (= e5 (op e1 e3)) (= e0 (op e1 e2))) (= e3 (op e4 e2))) (= e1 (op e3 e2))) (= e2 (op e4 e4)))))
(assert (not (and (and (and (and (= e5 (op e2 e3)) (= e0 (op e2 e1))) (= e3 (op e4 e1))) (= e2 (op e3 e1))) (= e1 (op e4 e4)))))
(assert (not (and (and (and (and (= e0 (op e3 e2)) (= e1 (op e3 e4))) (= e2 (op e5 e4))) (= e3 (op e2 e4))) (= e4 (op e5 e5)))))
(assert (not (and (and (and (and (= e0 (op e4 e2)) (= e1 (op e4 e3))) (= e2 (op e5 e3))) (= e4 (op e2 e3))) (= e3 (op e5 e5)))))
(assert (not (and (and (and (and (= e0 (op e2 e3)) (= e1 (op e2 e4))) (= e3 (op e5 e4))) (= e2 (op e3 e4))) (= e4 (op e5 e5)))))
(assert (not (and (and (and (and (= e0 (op e4 e3)) (= e1 (op e4 e2))) (= e3 (op e5 e2))) (= e4 (op e3 e2))) (= e2 (op e5 e5)))))
(assert (not (and (and (and (and (= e0 (op e2 e4)) (= e1 (op e2 e3))) (= e4 (op e5 e3))) (= e2 (op e4 e3))) (= e3 (op e5 e5)))))
(assert (not (and (and (and (and (= e0 (op e3 e4)) (= e1 (op e3 e2))) (= e4 (op e5 e2))) (= e3 (op e4 e2))) (= e2 (op e5 e5)))))
(assert (not (and (and (and (and (= e0 (op e3 e1)) (= e2 (op e3 e4))) (= e1 (op e5 e4))) (= e3 (op e1 e4))) (= e4 (op e5 e5)))))
(assert (not (and (and (and (and (= e0 (op e4 e1)) (= e2 (op e4 e3))) (= e1 (op e5 e3))) (= e4 (op e1 e3))) (= e3 (op e5 e5)))))
(assert (not (and (and (and (and (= e0 (op e1 e3)) (= e2 (op e1 e4))) (= e3 (op e5 e4))) (= e1 (op e3 e4))) (= e4 (op e5 e5)))))
(assert (not (and (and (and (and (= e0 (op e4 e3)) (= e2 (op e4 e1))) (= e3 (op e5 e1))) (= e4 (op e3 e1))) (= e1 (op e5 e5)))))
(assert (not (and (and (and (and (= e0 (op e1 e4)) (= e2 (op e1 e3))) (= e4 (op e5 e3))) (= e1 (op e4 e3))) (= e3 (op e5 e5)))))
(assert (not (and (and (and (and (= e0 (op e3 e4)) (= e2 (op e3 e1))) (= e4 (op e5 e1))) (= e3 (op e4 e1))) (= e1 (op e5 e5)))))
(assert (not (and (and (and (and (= e0 (op e2 e1)) (= e3 (op e2 e4))) (= e1 (op e5 e4))) (= e2 (op e1 e4))) (= e4 (op e5 e5)))))
(assert (not (and (and (and (and (= e0 (op e4 e1)) (= e3 (op e4 e2))) (= e1 (op e5 e2))) (= e4 (op e1 e2))) (= e2 (op e5 e5)))))
(assert (not (and (and (and (and (= e0 (op e1 e2)) (= e3 (op e1 e4))) (= e2 (op e5 e4))) (= e1 (op e2 e4))) (= e4 (op e5 e5)))))
(assert (not (and (and (and (and (= e0 (op e4 e2)) (= e3 (op e4 e1))) (= e2 (op e5 e1))) (= e4 (op e2 e1))) (= e1 (op e5 e5)))))
(assert (not (and (and (and (and (= e0 (op e1 e4)) (= e3 (op e1 e2))) (= e4 (op e5 e2))) (= e1 (op e4 e2))) (= e2 (op e5 e5)))))
(assert (not (and (and (and (and (= e0 (op e2 e4)) (= e3 (op e2 e1))) (= e4 (op e5 e1))) (= e2 (op e4 e1))) (= e1 (op e5 e5)))))
(assert (not (and (and (and (and (= e0 (op e2 e1)) (= e4 (op e2 e3))) (= e1 (op e5 e3))) (= e2 (op e1 e3))) (= e3 (op e5 e5)))))
(assert (not (and (and (and (and (= e0 (op e3 e1)) (= e4 (op e3 e2))) (= e1 (op e5 e2))) (= e3 (op e1 e2))) (= e2 (op e5 e5)))))
(assert (not (and (and (and (and (= e0 (op e1 e2)) (= e4 (op e1 e3))) (= e2 (op e5 e3))) (= e1 (op e2 e3))) (= e3 (op e5 e5)))))
(assert (not (and (and (and (and (= e0 (op e3 e2)) (= e4 (op e3 e1))) (= e2 (op e5 e1))) (= e3 (op e2 e1))) (= e1 (op e5 e5)))))
(assert (not (and (and (and (and (= e0 (op e1 e3)) (= e4 (op e1 e2))) (= e3 (op e5 e2))) (= e1 (op e3 e2))) (= e2 (op e5 e5)))))
(assert (not (and (and (and (and (= e0 (op e2 e3)) (= e4 (op e2 e1))) (= e3 (op e5 e1))) (= e2 (op e3 e1))) (= e1 (op e5 e5)))))
(assert (not (and (and (and (and (= e1 (op e3 e2)) (= e0 (op e3 e4))) (= e2 (op e5 e4))) (= e3 (op e2 e4))) (= e4 (op e5 e5)))))
(assert (not (and (and (and (and (= e1 (op e4 e2)) (= e0 (op e4 e3))) (= e2 (op e5 e3))) (= e4 (op e2 e3))) (= e3 (op e5 e5)))))
(assert (not (and (and (and (and (= e1 (op e2 e3)) (= e0 (op e2 e4))) (= e3 (op e5 e4))) (= e2 (op e3 e4))) (= e4 (op e5 e5)))))
(assert (not (and (and (and (and (= e1 (op e4 e3)) (= e0 (op e4 e2))) (= e3 (op e5 e2))) (= e4 (op e3 e2))) (= e2 (op e5 e5)))))
(assert (not (and (and (and (and (= e1 (op e2 e4)) (= e0 (op e2 e3))) (= e4 (op e5 e3))) (= e2 (op e4 e3))) (= e3 (op e5 e5)))))
(assert (not (and (and (and (and (= e1 (op e3 e4)) (= e0 (op e3 e2))) (= e4 (op e5 e2))) (= e3 (op e4 e2))) (= e2 (op e5 e5)))))
(assert (not (and (and (and (and (= e2 (op e3 e1)) (= e0 (op e3 e4))) (= e1 (op e5 e4))) (= e3 (op e1 e4))) (= e4 (op e5 e5)))))
(assert (not (and (and (and (and (= e2 (op e4 e1)) (= e0 (op e4 e3))) (= e1 (op e5 e3))) (= e4 (op e1 e3))) (= e3 (op e5 e5)))))
(assert (not (and (and (and (and (= e2 (op e1 e3)) (= e0 (op e1 e4))) (= e3 (op e5 e4))) (= e1 (op e3 e4))) (= e4 (op e5 e5)))))
(assert (not (and (and (and (and (= e2 (op e4 e3)) (= e0 (op e4 e1))) (= e3 (op e5 e1))) (= e4 (op e3 e1))) (= e1 (op e5 e5)))))
(assert (not (and (and (and (and (= e2 (op e1 e4)) (= e0 (op e1 e3))) (= e4 (op e5 e3))) (= e1 (op e4 e3))) (= e3 (op e5 e5)))))
(assert (not (and (and (and (and (= e2 (op e3 e4)) (= e0 (op e3 e1))) (= e4 (op e5 e1))) (= e3 (op e4 e1))) (= e1 (op e5 e5)))))
(assert (not (and (and (and (and (= e3 (op e2 e1)) (= e0 (op e2 e4))) (= e1 (op e5 e4))) (= e2 (op e1 e4))) (= e4 (op e5 e5)))))
(assert (not (and (and (and (and (= e3 (op e4 e1)) (= e0 (op e4 e2))) (= e1 (op e5 e2))) (= e4 (op e1 e2))) (= e2 (op e5 e5)))))
(assert (not (and (and (and (and (= e3 (op e1 e2)) (= e0 (op e1 e4))) (= e2 (op e5 e4))) (= e1 (op e2 e4))) (= e4 (op e5 e5)))))
(assert (not (and (and (and (and (= e3 (op e4 e2)) (= e0 (op e4 e1))) (= e2 (op e5 e1))) (= e4 (op e2 e1))) (= e1 (op e5 e5)))))
(assert (not (and (and (and (and (= e3 (op e1 e4)) (= e0 (op e1 e2))) (= e4 (op e5 e2))) (= e1 (op e4 e2))) (= e2 (op e5 e5)))))
(assert (not (and (and (and (and (= e3 (op e2 e4)) (= e0 (op e2 e1))) (= e4 (op e5 e1))) (= e2 (op e4 e1))) (= e1 (op e5 e5)))))
(assert (not (and (and (and (and (= e4 (op e2 e1)) (= e0 (op e2 e3))) (= e1 (op e5 e3))) (= e2 (op e1 e3))) (= e3 (op e5 e5)))))
(assert (not (and (and (and (and (= e4 (op e3 e1)) (= e0 (op e3 e2))) (= e1 (op e5 e2))) (= e3 (op e1 e2))) (= e2 (op e5 e5)))))
(assert (not (and (and (and (and (= e4 (op e1 e2)) (= e0 (op e1 e3))) (= e2 (op e5 e3))) (= e1 (op e2 e3))) (= e3 (op e5 e5)))))
(assert (not (and (and (and (and (= e4 (op e3 e2)) (= e0 (op e3 e1))) (= e2 (op e5 e1))) (= e3 (op e2 e1))) (= e1 (op e5 e5)))))
(assert (not (and (and (and (and (= e4 (op e1 e3)) (= e0 (op e1 e2))) (= e3 (op e5 e2))) (= e1 (op e3 e2))) (= e2 (op e5 e5)))))
(assert (not (and (and (and (and (= e4 (op e2 e3)) (= e0 (op e2 e1))) (= e3 (op e5 e1))) (= e2 (op e3 e1))) (= e1 (op e5 e5)))))
(check-sat)
(exit)